# HG changeset patch # User wenzelm # Date 1283529828 -7200 # Node ID 01214c68f8bccea14fa8d52eb74bb22a6a178a5d # Parent 91d2a9844d574f89b9f01357860916e25fff1193# Parent dd043196150758e1ee53cd6c7153e2cf1c246086 merged diff -r 91d2a9844d57 -r 01214c68f8bc src/HOL/Import/proof_kernel.ML --- 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 "^ diff -r 91d2a9844d57 -r 01214c68f8bc src/HOL/Tools/Nitpick/nitpick_model.ML --- 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) = diff -r 91d2a9844d57 -r 01214c68f8bc src/HOL/Tools/Nitpick/nitpick_scope.ML --- 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 = diff -r 91d2a9844d57 -r 01214c68f8bc src/HOL/Tools/Nitpick/nitpick_util.ML --- 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 diff -r 91d2a9844d57 -r 01214c68f8bc src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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 ^ " :: " ^ diff -r 91d2a9844d57 -r 01214c68f8bc src/HOLCF/IOA/ABP/Correctness.thy --- 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" diff -r 91d2a9844d57 -r 01214c68f8bc src/HOLCF/IOA/ABP/ROOT.ML --- 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"]; diff -r 91d2a9844d57 -r 01214c68f8bc src/HOLCF/IOA/Storage/ROOT.ML --- 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"]; diff -r 91d2a9844d57 -r 01214c68f8bc src/Pure/Isar/attrib.ML --- 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; diff -r 91d2a9844d57 -r 01214c68f8bc src/Pure/Syntax/printer.ML --- 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; diff -r 91d2a9844d57 -r 01214c68f8bc src/Pure/config.ML --- 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; diff -r 91d2a9844d57 -r 01214c68f8bc src/Pure/goal_display.ML --- 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 = diff -r 91d2a9844d57 -r 01214c68f8bc src/Pure/meta_simplifier.ML --- 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 = diff -r 91d2a9844d57 -r 01214c68f8bc src/Pure/unify.ML --- 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;