--- a/src/HOL/Import/proof_kernel.ML Fri Sep 03 16:08:19 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Sep 03 18:03:48 2010 +0200
@@ -187,43 +187,40 @@
fun quotename c =
if Syntax.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
-fun simple_smart_string_of_cterm ct =
+fun simple_smart_string_of_cterm ctxt0 ct =
let
- val thy = Thm.theory_of_cterm ct;
+ val ctxt = Config.put show_all_types true ctxt0;
val {t,T,...} = rep_cterm ct
(* Hack to avoid parse errors with Trueprop *)
- val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
- handle TERM _ => ct)
+ val ct = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
+ handle TERM _ => ct
in
quote (
Print_Mode.setmp [] (
setmp_CRITICAL show_brackets false (
- setmp_CRITICAL show_all_types true (
setmp_CRITICAL Syntax.ambiguity_is_error false (
- setmp_CRITICAL show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
+ setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of))))
ct)
end
exception SMART_STRING
-fun smart_string_of_cterm ct =
+fun smart_string_of_cterm ctxt ct =
let
- val thy = Thm.theory_of_cterm ct
- val ctxt = ProofContext.init_global thy
val {t,T,...} = rep_cterm ct
(* Hack to avoid parse errors with Trueprop *)
- val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
- handle TERM _ => ct)
+ val ct = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
+ handle TERM _ => ct
fun match u = t aconv u
- fun G 0 = setmp_CRITICAL show_types true (setmp_CRITICAL show_sorts true)
- | G 1 = setmp_CRITICAL show_brackets true (G 0)
- | G 2 = setmp_CRITICAL show_all_types true (G 0)
- | G 3 = setmp_CRITICAL show_brackets true (G 2)
- | G _ = raise SMART_STRING
+ fun G 0 f ctxt x = setmp_CRITICAL show_types true (setmp_CRITICAL show_sorts true) (f ctxt) x
+ | G 1 f ctxt x = setmp_CRITICAL show_brackets true (G 0) f ctxt x
+ | G 2 f ctxt x = G 0 f (Config.put show_all_types true ctxt) x
+ | G 3 f ctxt x = setmp_CRITICAL show_brackets true (G 2) f ctxt x
+ | G _ _ _ _ = raise SMART_STRING
fun F n =
let
val str =
- setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
+ setmp_CRITICAL show_brackets false (G n Syntax.string_of_term ctxt) (term_of ct)
val u = Syntax.parse_term ctxt str
|> Type_Infer.constrain T |> Syntax.check_term ctxt
in
@@ -233,13 +230,13 @@
end
handle ERROR mesg => F (n + 1)
| SMART_STRING =>
- error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
+ error ("smart_string failed for: "^ G 0 Syntax.string_of_term ctxt (term_of ct))
in
Print_Mode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
end
- handle ERROR mesg => simple_smart_string_of_cterm ct
+ handle ERROR mesg => simple_smart_string_of_cterm ctxt ct
-val smart_string_of_thm = smart_string_of_cterm o cprop_of
+fun smart_string_of_thm ctxt = smart_string_of_cterm ctxt o cprop_of
fun prth th = writeln (Print_Mode.setmp [] Display.string_of_thm_without_context th);
fun prin t = writeln (Print_Mode.setmp []
@@ -366,9 +363,6 @@
val scan_start_of_tag = $$ #"<" |-- scan_id --
repeat ($$ #" " |-- scan_attribute)
-(* The evaluation delay introduced through the 'toks' argument is needed
-for the sake of the SML/NJ (110.9.1) compiler. Either that or an explicit
-type :-( *)
fun scan_end_of_tag toks = ($$ #"/" |-- $$ #">" |-- succeed []) toks
val scan_end_tag = $$ #"<" |-- $$ #"/" |-- scan_id --| $$ #">"
@@ -1369,11 +1363,13 @@
val thy' = add_hol4_pending thyname thmname args thy
val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
val th = disambiguate_frees th
- val thy2 = if gen_output
- then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
- (smart_string_of_thm th) ^ "\n by (import " ^
- thyname ^ " " ^ (quotename thmname) ^ ")") thy'
- else thy'
+ val thy2 =
+ if gen_output
+ then
+ add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
+ (smart_string_of_thm (Syntax.init_pretty_global thy') th) ^ "\n by (import " ^
+ thyname ^ " " ^ (quotename thmname) ^ ")") thy'
+ else thy'
in
(thy2,hth')
end
@@ -1934,21 +1930,25 @@
val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
val rew = rewrite_hol4_term eq thy''
val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
- val thy22 = if Thm.def_name constname = thmname andalso not redeclared andalso csyn = NoSyn
- then
- let
- val p1 = quotename constname
- val p2 = Syntax.string_of_typ_global thy'' ctype
- val p3 = string_of_mixfix csyn
- val p4 = smart_string_of_cterm crhs
- in
- add_dump ("definition\n " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ " where\n " ^ p4) thy''
- end
- else
- add_dump ("consts\n " ^ quotename constname ^ " :: \"" ^
- Syntax.string_of_typ_global thy'' ctype ^
- "\" " ^ string_of_mixfix csyn ^ "\n\ndefs\n " ^
- quotename thmname ^ ": " ^ smart_string_of_cterm crhs) thy''
+ val thy22 =
+ if Thm.def_name constname = thmname andalso not redeclared andalso csyn = NoSyn
+ then
+ let
+ val ctxt = Syntax.init_pretty_global thy''
+ val p1 = quotename constname
+ val p2 = Syntax.string_of_typ ctxt ctype
+ val p3 = string_of_mixfix csyn
+ val p4 = smart_string_of_cterm ctxt crhs
+ in
+ add_dump ("definition\n " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ " where\n " ^ p4) thy''
+ end
+ else
+ let val ctxt = Syntax.init_pretty_global thy'' in
+ add_dump ("consts\n " ^ quotename constname ^ " :: \"" ^
+ Syntax.string_of_typ ctxt ctype ^
+ "\" " ^ string_of_mixfix csyn ^ "\n\ndefs\n " ^
+ quotename thmname ^ ": " ^ smart_string_of_cterm ctxt crhs) thy''
+ end
val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
SOME (_,res) => HOLThm(rens_of linfo,res)
| NONE => raise ERR "new_definition" "Bad conclusion"
@@ -2043,9 +2043,11 @@
in
(name'::names,thy')
end) names ([], thy')
- val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^
- "\n by (import " ^ thyname ^ " " ^ thmname ^ ")")
- thy'
+ val thy'' =
+ add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^
+ (smart_string_of_thm (Syntax.init_pretty_global thy') th) ^
+ "\n by (import " ^ thyname ^ " " ^ thmname ^ ")")
+ thy'
val _ = message "RESULT:"
val _ = if_debug pth hth
in
@@ -2118,9 +2120,10 @@
val tnames_string = if null tnames
then ""
else "(" ^ commas tnames ^ ") "
- val proc_prop = if null tnames
- then smart_string_of_cterm
- else setmp_CRITICAL show_all_types true smart_string_of_cterm
+ val proc_prop =
+ smart_string_of_cterm
+ (Syntax.init_pretty_global thy4
+ |> not (null tnames) ? Config.put show_all_types true)
val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
^ (string_of_mixfix tsyn) ^ "\n by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
@@ -2201,9 +2204,10 @@
val tnames_string = if null tnames
then ""
else "(" ^ commas tnames ^ ") "
- val proc_prop = if null tnames
- then smart_string_of_cterm
- else setmp_CRITICAL show_all_types true smart_string_of_cterm
+ val proc_prop =
+ smart_string_of_cterm
+ (Syntax.init_pretty_global thy4
+ |> not (null tnames) ? Config.put show_all_types true)
val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
" = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^
(string_of_mixfix tsyn) ^ " morphisms "^
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Sep 03 16:08:19 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Sep 03 18:03:48 2010 +0200
@@ -949,7 +949,7 @@
T T' (rep_of name)
in
Pretty.block (Pretty.breaks
- [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
+ [Syntax.pretty_term (set_show_all_types ctxt) t1,
Pretty.str oper, Syntax.pretty_term ctxt t2])
end
fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Sep 03 16:08:19 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Sep 03 18:03:48 2010 +0200
@@ -142,9 +142,10 @@
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
fun quintuple_for_scope code_type code_term code_string
- ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
+ ({hol_ctxt = {ctxt = ctxt0, stds, ...}, card_assigns, bits, bisim_depth,
datatypes, ...} : scope) =
let
+ val ctxt = set_show_all_types ctxt0
val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
@{typ bisim_iterator}]
val (iter_assigns, card_assigns) =
@@ -175,9 +176,8 @@
(if bisim_depth < 0 andalso forall (not o #co) datatypes then []
else [code_string ("bisim_depth = " ^ signed_string_of_int bisim_depth)])
in
- setmp_show_all_types
- (fn () => (cards primary_card_assigns, cards secondary_card_assigns,
- maxes (), iters (), miscs ())) ()
+ (cards primary_card_assigns, cards secondary_card_assigns,
+ maxes (), iters (), miscs ())
end
fun pretties_for_scope scope verbose =
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Sep 03 16:08:19 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Sep 03 18:03:48 2010 +0200
@@ -71,7 +71,7 @@
val eta_expand : typ list -> term -> int -> term
val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
- val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
+ val set_show_all_types : Proof.context -> Proof.context
val indent_size : int
val pstrs : string -> Pretty.T list
val unyxml : string -> string
@@ -279,9 +279,9 @@
fun DETERM_TIMEOUT delay tac st =
Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
-fun setmp_show_all_types f =
- setmp_CRITICAL show_all_types
- (!show_types orelse !show_sorts orelse !show_all_types) f
+fun set_show_all_types ctxt =
+ Config.put show_all_types
+ (!show_types orelse !show_sorts orelse Config.get ctxt show_all_types) ctxt
val indent_size = 2
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 03 16:08:19 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 03 18:03:48 2010 +0200
@@ -945,13 +945,13 @@
step :: aux subst depth nextp proof
in aux [] 0 (1, 1) end
-fun string_for_proof ctxt full_types i n =
+fun string_for_proof ctxt0 full_types i n =
let
+ val ctxt = Config.put show_free_types false ctxt0
fun fix_print_mode f x =
- setmp_CRITICAL show_no_free_types true
- (setmp_CRITICAL show_types true
- (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
- (print_mode_value ())) f)) x
+ setmp_CRITICAL show_types true
+ (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+ (print_mode_value ())) f) x
fun do_indent ind = replicate_string (ind * indent_size) " "
fun do_free (s, T) =
maybe_quote s ^ " :: " ^
--- a/src/HOLCF/IOA/ABP/Correctness.thy Fri Sep 03 16:08:19 2010 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.thy Fri Sep 03 18:03:48 2010 +0200
@@ -6,6 +6,7 @@
theory Correctness
imports IOA Env Impl Impl_finite
+uses "Check.ML"
begin
primrec reduce :: "'a list => 'a list"
--- a/src/HOLCF/IOA/ABP/ROOT.ML Fri Sep 03 16:08:19 2010 +0200
+++ b/src/HOLCF/IOA/ABP/ROOT.ML Fri Sep 03 18:03:48 2010 +0200
@@ -4,8 +4,4 @@
This is the ROOT file for the Alternating Bit Protocol performed in
I/O-Automata.
*)
-
-goals_limit := 1;
-
-use "Check.ML";
use_thys ["Correctness"];
--- a/src/HOLCF/IOA/Storage/ROOT.ML Fri Sep 03 16:08:19 2010 +0200
+++ b/src/HOLCF/IOA/Storage/ROOT.ML Fri Sep 03 18:03:48 2010 +0200
@@ -3,7 +3,4 @@
Memory storage case study.
*)
-
-goals_limit := 1;
-
use_thys ["Correctness"];
--- a/src/Pure/Isar/attrib.ML Fri Sep 03 16:08:19 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Sep 03 18:03:48 2010 +0200
@@ -374,7 +374,7 @@
fun declare_config make coerce global name default =
let
- val config_value = Config.declare global name (make o default);
+ val config_value = Config.declare_generic {global = global} name (make o default);
val config = coerce config_value;
in (config, register_config config_value) end;
--- a/src/Pure/Syntax/printer.ML Fri Sep 03 16:08:19 2010 +0200
+++ b/src/Pure/Syntax/printer.ML Fri Sep 03 18:03:48 2010 +0200
@@ -9,8 +9,8 @@
val show_brackets: bool Unsynchronized.ref
val show_sorts: bool Unsynchronized.ref
val show_types: bool Unsynchronized.ref
- val show_no_free_types: bool Unsynchronized.ref
- val show_all_types: bool Unsynchronized.ref
+ val show_free_types: bool Config.T
+ val show_all_types: bool Config.T
val show_structs: bool Unsynchronized.ref
val show_question_marks_default: bool Unsynchronized.ref
val show_question_marks_value: Config.value Config.T
@@ -51,13 +51,13 @@
val show_types = Unsynchronized.ref false;
val show_sorts = Unsynchronized.ref false;
val show_brackets = Unsynchronized.ref false;
-val show_no_free_types = Unsynchronized.ref false;
-val show_all_types = Unsynchronized.ref false;
+val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
+val show_all_types = Config.bool (Config.declare "show_all_types" (fn _ => Config.Bool false));
val show_structs = Unsynchronized.ref false;
val show_question_marks_default = Unsynchronized.ref true;
val show_question_marks_value =
- Config.declare false "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
+ Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
val show_question_marks = Config.bool show_question_marks_value;
fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
@@ -119,9 +119,11 @@
(** term_to_ast **)
-fun ast_of_term idents consts ctxt trf
- show_all_types no_freeTs show_types show_sorts show_structs tm =
+fun ast_of_term idents consts ctxt trf show_types show_sorts show_structs tm =
let
+ val show_free_types = Config.get ctxt show_free_types;
+ val show_all_types = Config.get ctxt show_all_types;
+
val {structs, fixes} = idents;
fun mark_atoms ((t as Const (c, T)) $ u) =
@@ -148,11 +150,11 @@
fun prune_typs (t_seen as (Const _, _)) = t_seen
| prune_typs (t as Free (x, ty), seen) =
if ty = dummyT then (t, seen)
- else if no_freeTs orelse member (op aconv) seen t then (Lexicon.free x, seen)
+ else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
else (t, t :: seen)
| prune_typs (t as Var (xi, ty), seen) =
if ty = dummyT then (t, seen)
- else if no_freeTs orelse member (op aconv) seen t then (Lexicon.var xi, seen)
+ else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
else (t, t :: seen)
| prune_typs (t_seen as (Bound _, _)) = t_seen
| prune_typs (Abs (x, ty, t), seen) =
@@ -199,8 +201,9 @@
end;
fun term_to_ast idents consts ctxt trf tm =
- ast_of_term idents consts ctxt trf (! show_all_types) (! show_no_free_types)
- (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) (! show_structs) tm;
+ ast_of_term idents consts ctxt trf
+ (! show_types orelse ! show_sorts orelse Config.get ctxt show_all_types)
+ (! show_sorts) (! show_structs) tm;
--- a/src/Pure/config.ML Fri Sep 03 16:08:19 2010 +0200
+++ b/src/Pure/config.ML Fri Sep 03 18:03:48 2010 +0200
@@ -22,7 +22,9 @@
val get_generic: Context.generic -> 'a T -> 'a
val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
- val declare: bool -> string -> (Context.generic -> value) -> value T
+ val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> value T
+ val declare_global: string -> (Context.generic -> value) -> value T
+ val declare: string -> (Context.generic -> value) -> value T
val name_of: 'a T -> string
end;
@@ -98,7 +100,7 @@
fun merge data = Inttab.merge (K true) data;
);
-fun declare global name default =
+fun declare_generic {global} name default =
let
val id = serial ();
@@ -120,6 +122,9 @@
| map_value f context = update_value f context;
in Config {name = name, get_value = get_value, map_value = map_value} end;
+val declare_global = declare_generic {global = true};
+val declare = declare_generic {global = false};
+
fun name_of (Config {name, ...}) = name;
--- a/src/Pure/goal_display.ML Fri Sep 03 16:08:19 2010 +0200
+++ b/src/Pure/goal_display.ML Fri Sep 03 18:03:48 2010 +0200
@@ -24,8 +24,7 @@
(*true: show consts with types in proof state output*)
val show_consts_default = Unsynchronized.ref false;
-val show_consts_value =
- Config.declare false "show_consts" (fn _ => Config.Bool (! show_consts_default));
+val show_consts_value = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
val show_consts = Config.bool show_consts_value;
fun pretty_flexpair ctxt (t, u) = Pretty.block
@@ -63,8 +62,11 @@
in
-fun pretty_goals ctxt {total, main, maxgoals} state =
+fun pretty_goals ctxt0 {total, main, maxgoals} state =
let
+ val ctxt = Config.put show_free_types false ctxt0;
+ val show_all_types = Config.get ctxt show_all_types;
+
val prt_sort = Syntax.pretty_sort ctxt;
val prt_typ = Syntax.pretty_typ ctxt;
val prt_term = Syntax.pretty_term ctxt;
@@ -115,10 +117,9 @@
(if types then pretty_vars prop else []) @
(if sorts then pretty_varsT prop else []);
in
- setmp_CRITICAL show_no_free_types true
- (setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
- (setmp_CRITICAL show_sorts false pretty_gs))
- (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
+ setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse show_all_types)
+ (setmp_CRITICAL show_sorts false pretty_gs)
+ (! show_types orelse ! show_sorts orelse show_all_types, ! show_sorts)
end;
fun pretty_goals_without_context n th =
--- a/src/Pure/meta_simplifier.ML Fri Sep 03 16:08:19 2010 +0200
+++ b/src/Pure/meta_simplifier.ML Fri Sep 03 18:03:48 2010 +0200
@@ -250,7 +250,7 @@
(* simp depth *)
-val simp_depth_limit_value = Config.declare false "simp_depth_limit" (K (Config.Int 100));
+val simp_depth_limit_value = Config.declare "simp_depth_limit" (K (Config.Int 100));
val simp_depth_limit = Config.int simp_depth_limit_value;
val trace_simp_depth_limit = Unsynchronized.ref 1;
@@ -273,12 +273,11 @@
exception SIMPLIFIER of string * thm;
-val debug_simp_value = Config.declare false "debug_simp" (K (Config.Bool false));
+val debug_simp_value = Config.declare "debug_simp" (K (Config.Bool false));
val debug_simp = Config.bool debug_simp_value;
val trace_simp_default = Unsynchronized.ref false;
-val trace_simp_value =
- Config.declare false "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
+val trace_simp_value = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
val trace_simp = Config.bool trace_simp_value;
fun if_enabled (Simpset ({context, ...}, _)) flag f =
--- a/src/Pure/unify.ML Fri Sep 03 16:08:19 2010 +0200
+++ b/src/Pure/unify.ML Fri Sep 03 18:03:48 2010 +0200
@@ -32,19 +32,19 @@
(*Unification options*)
(*tracing starts above this depth, 0 for full*)
-val trace_bound_value = Config.declare true "unify_trace_bound" (K (Config.Int 50));
+val trace_bound_value = Config.declare_global "unify_trace_bound" (K (Config.Int 50));
val trace_bound = Config.int trace_bound_value;
(*unification quits above this depth*)
-val search_bound_value = Config.declare true "unify_search_bound" (K (Config.Int 60));
+val search_bound_value = Config.declare_global "unify_search_bound" (K (Config.Int 60));
val search_bound = Config.int search_bound_value;
(*print dpairs before calling SIMPL*)
-val trace_simp_value = Config.declare true "unify_trace_simp" (K (Config.Bool false));
+val trace_simp_value = Config.declare_global "unify_trace_simp" (K (Config.Bool false));
val trace_simp = Config.bool trace_simp_value;
(*announce potential incompleteness of type unification*)
-val trace_types_value = Config.declare true "unify_trace_types" (K (Config.Bool false));
+val trace_types_value = Config.declare_global "unify_trace_types" (K (Config.Bool false));
val trace_types = Config.bool trace_types_value;