# HG changeset patch # User wenzelm # Date 1717928944 -7200 # Node ID 026c4ad6f23e8e1228da2c905a74ba1bdfcb6293 # Parent 11fee9e6ba436b1c9e0d5e167f763a1321ef936a tuned; diff -r 11fee9e6ba43 -r 026c4ad6f23e src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Sat Jun 08 23:17:20 2024 +0200 +++ b/src/Pure/raw_simplifier.ML Sun Jun 09 12:29:04 2024 +0200 @@ -446,6 +446,8 @@ fun print_thm ctxt s (name, th) = print_term ctxt (if name = "" then s else s ^ " " ^ quote name ^ ":") (Thm.full_prop_of th); +fun print_thm0 ctxt msg th = print_thm ctxt msg ("", th); + (** simpset operations **) @@ -466,8 +468,7 @@ (Net.delete_term eq_rrule (Thm.term_of elhs, rrule) rules, prems, depth)) handle Net.DELETE => (if not loud then () - else cond_warning ctxt - (fn () => print_thm ctxt "Rewrite rule not in simpset:" ("", thm)); + else cond_warning ctxt (fn () => print_thm0 ctxt "Rewrite rule not in simpset:" thm); ctxt); fun insert_rrule (rrule as {thm, name, ...}) ctxt = @@ -478,8 +479,7 @@ val rules' = Net.insert_term eq_rrule (Thm.term_of elhs, trim_context_rrule rrule2) rules; in (rules', prems, depth) end) handle Net.INSERT => - (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm)); - ctxt)); + (cond_warning ctxt (fn () => print_thm0 ctxt "Ignoring duplicate rewrite rule:" thm); ctxt)); val vars_set = Vars.build o Vars.add_vars; @@ -603,7 +603,7 @@ false) handle Net.INSERT => (cond_warning ctxt - (fn () => print_thm ctxt "Symmetric rewrite rule already in simpset:" ("", thm)); + (fn () => print_thm0 ctxt "Symmetric rewrite rule already in simpset:" thm); true); fun sym_present ctxt thms = @@ -631,7 +631,7 @@ (* with check for presence of symmetric version: if sym_present ctxt [thm] - then (cond_warning ctxt (fn () => print_thm ctxt "Ignoring rewrite rule:" ("", thm)); ctxt) + then (cond_warning ctxt (fn () => print_thm0 ctxt "Ignoring rewrite rule:" thm); ctxt) else ctxt addsimps [thm]; *) fun del_simp thm ctxt = ctxt delsimps [thm]; @@ -910,16 +910,14 @@ Thm.transitive thm (Drule.beta_eta_conversion (Thm.rhs_of thm)) in Thm.transitive nthm nthm' end end - val _ = - if msg then cond_tracing ctxt (fn () => print_thm ctxt "SUCCEEDED" ("", thm')) - else (); + val _ = if msg then cond_tracing ctxt (fn () => print_thm0 ctxt "SUCCEEDED" thm') else (); in SOME thm'' end handle THM _ => let val _ $ _ $ prop0 = Thm.prop_of thm; val _ = cond_tracing ctxt (fn () => - print_thm ctxt "Proved wrong theorem (bad subgoaler?)" ("", thm') ^ "\n" ^ + print_thm0 ctxt "Proved wrong theorem (bad subgoaler?)" thm' ^ "\n" ^ print_term ctxt "Should have proved:" prop0); in NONE end; @@ -932,7 +930,7 @@ val thm' = Thm.close_derivation \<^here> thm; in if rewrite_rule_extra_vars prems lhs rhs - then (cond_warning ctxt (fn () => print_thm ctxt "Extra vars on rhs:" ("", thm)); []) + then (cond_warning ctxt (fn () => print_thm0 ctxt "Extra vars on rhs:" thm); []) else [mk_rrule2 {thm = thm', name = "", lhs = lhs, elhs = elhs, perm = false}] end; @@ -1007,27 +1005,27 @@ then (cond_tracing ctxt (fn () => print_thm ctxt "Cannot apply permutative rewrite rule" (name, thm) ^ "\n" ^ - print_thm ctxt "Term does not become smaller:" ("", thm')); + print_thm0 ctxt "Term does not become smaller:" thm'); NONE) else (cond_tracing ctxt (fn () => print_thm ctxt "Applying instance of rewrite rule" (name, thm)); if unconditional then - (cond_tracing ctxt (fn () => print_thm ctxt "Rewriting:" ("", thm')); + (cond_tracing ctxt (fn () => print_thm0 ctxt "Rewriting:" thm'); trace_rrule trace_args ctxt (fn ctxt' => let val lr = Logic.dest_equals prop; val SOME thm'' = check_conv ctxt' false eta_thm thm'; in SOME (thm'', uncond_skel (congs, lr)) end)) else - (cond_tracing ctxt (fn () => print_thm ctxt "Trying to rewrite:" ("", thm')); + (cond_tracing ctxt (fn () => print_thm0 ctxt "Trying to rewrite:" thm'); if simp_depth ctxt > Config.get ctxt simp_depth_limit then (cond_tracing ctxt (fn () => "simp_depth_limit exceeded - giving up"); NONE) else trace_rrule trace_args ctxt (fn ctxt' => (case prover ctxt' thm' of - NONE => (cond_tracing ctxt' (fn () => print_thm ctxt' "FAILED" ("", thm')); NONE) + NONE => (cond_tracing ctxt' (fn () => print_thm0 ctxt' "FAILED" thm'); NONE) | SOME thm2 => (case check_conv ctxt' true eta_thm thm2 of NONE => NONE @@ -1069,8 +1067,7 @@ NONE => (cond_tracing' ctxt simp_debug (fn () => "FAILED"); proc_rews ps) | SOME raw_thm => (cond_tracing ctxt (fn () => - print_thm ctxt ("Procedure " ^ quote name ^ " produced rewrite rule:") - ("", raw_thm)); + print_thm0 ctxt ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm); (case rews (mk_procrule ctxt raw_thm) of NONE => (cond_tracing ctxt (fn () => @@ -1101,9 +1098,8 @@ is handled when congc is called *) val thm' = Thm.instantiate insts (Thm.rename_boundvars (Thm.term_of rlhs) (Thm.term_of t) rthm); - val _ = - cond_tracing ctxt (fn () => print_thm ctxt "Applying congruence rule:" ("", thm')); - fun err (msg, thm) = (cond_tracing ctxt (fn () => print_thm ctxt msg ("", thm)); NONE); + val _ = cond_tracing ctxt (fn () => print_thm0 ctxt "Applying congruence rule:" thm'); + fun err (msg, thm) = (cond_tracing ctxt (fn () => print_thm0 ctxt msg thm); NONE); in (case prover thm' of NONE => err ("Congruence proof failed. Could not prove", thm')