Explicit references in antiquotations in typing.ML. Move trace switch definition to HoTT_Base.

2 files changed, 6 insertions, 6 deletions

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index ed8c18b..23e51e5 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -27,6 +27,9 @@ section \<open>Setup non-core logic functionality\<close>
 
 declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close>
 
+ML \<open>val trace = Attrib.setup_config_bool @{binding "trace"} (K false)\<close>
+  \<comment> \<open>Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on.\<close>
+
 text \<open>The following file sets up type assumption and inference functionality.\<close>
 
 ML_file "typing.ML"
diff --git a/typing.ML b/typing.ML
index 4bcb633..2a049d4 100644
--- a/typing.ML
+++ b/typing.ML
@@ -6,9 +6,6 @@ Functionality for object-level type inference.
 
 ********)
 
-(* Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on *)
-val trace = Attrib.setup_config_bool @{binding "trace"} (K false)
-
 (* ====================================== Helper functions ====================================== *)
 
 signature TYPING_LIB =
@@ -104,14 +101,14 @@ struct
 type jmt = term
 
 (* Determine if a term is a typing judgment *)
-fun is_typing_jmt (@{const has_type} $ _ $ _) = true
+fun is_typing_jmt (@{const HoTT_Base.has_type} $ _ $ _) = true
   | is_typing_jmt _ = false
 
 (* Functions to extract a and A from propositions "a: A" *)
-fun term_of_jmt (@{const has_type} $ t $ _) = t
+fun term_of_jmt (@{const HoTT_Base.has_type} $ t $ _) = t
   | term_of_jmt _ = Exn.error "Not a typing judgment"
 
-fun type_of_jmt (@{const has_type} $ _ $ T) = T
+fun type_of_jmt (@{const HoTT_Base.has_type} $ _ $ T) = T
   | type_of_jmt _ = Exn.error "Not a typing judgment"
 
 (* Get typing assumptions in "this" *)