# HG changeset patch
# User wenzelm
# Date 1697548214 -7200
# Node ID 8f4424187193549a50f0994bac575cd2bdfc61d4
# Parent  a7e4b412cc7c625d9bdb9e726fe8b1dae41f9955
more standard ML setup;
proper tracing messages depending on context option, not Unsynchronized.ref;
tuned whitespace;

diff -r a7e4b412cc7c -r 8f4424187193 src/ZF/Datatype.thy
--- a/src/ZF/Datatype.thy	Tue Oct 17 12:10:58 2023 +0200
+++ b/src/ZF/Datatype.thy	Tue Oct 17 15:10:14 2023 +0200
@@ -58,63 +58,63 @@
 
 
 
-(*Simproc for freeness reasoning: compare datatype constructors for equality*)
-structure DataFree =
+(* Simproc for freeness reasoning: compare datatype constructors for equality *)
+
+structure Data_Free:
+sig
+  val trace: bool Config.T
+  val proc: Proof.context -> cterm -> thm option
+end =
 struct
-  val trace = Unsynchronized.ref false;
+
+val trace = Attrib.setup_config_bool \<^binding>\<open>data_free_trace\<close> (K false);
 
-  fun mk_new ([],[]) = \<^Const>\<open>True\<close>
-    | mk_new (largs,rargs) =
-        Balanced_Tree.make FOLogic.mk_conj
+fun mk_new ([],[]) = \<^Const>\<open>True\<close>
+  | mk_new (largs,rargs) =
+      Balanced_Tree.make FOLogic.mk_conj
                  (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
 
- val datatype_ss = simpset_of \<^context>;
+val datatype_ss = simpset_of \<^context>;
 
- fun proc ctxt ct =
-   let val old = Thm.term_of ct
-       val thy = Proof_Context.theory_of ctxt
-       val _ =
-         if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term ctxt old)
-         else ()
-       val (lhs,rhs) = FOLogic.dest_eq old
-       val (lhead, largs) = strip_comb lhs
-       and (rhead, rargs) = strip_comb rhs
-       val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
-       val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
-       val lcon_info = the (Symtab.lookup (ConstructorsData.get thy) lname)
-         handle Option.Option => raise Match;
-       val rcon_info = the (Symtab.lookup (ConstructorsData.get thy) rname)
-         handle Option.Option => raise Match;
-       val new =
-           if #big_rec_name lcon_info = #big_rec_name rcon_info
-               andalso not (null (#free_iffs lcon_info)) then
-               if lname = rname then mk_new (largs, rargs)
-               else \<^Const>\<open>False\<close>
-           else raise Match
-       val _ =
-         if !trace then writeln ("NEW = " ^ Syntax.string_of_term ctxt new)
-         else ();
-       val goal = Logic.mk_equals (old, new)
-       val thm = Goal.prove ctxt [] [] goal
-         (fn _ => resolve_tac ctxt @{thms iff_reflection} 1 THEN
-           simp_tac (put_simpset datatype_ss ctxt addsimps
-            (map (Thm.transfer thy) (#free_iffs lcon_info))) 1)
-         handle ERROR msg =>
-         (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal);
-          raise Match)
-   in SOME thm end
-   handle Match => NONE;
-
-
-  val conv =
-    Simplifier.make_simproc \<^context> "data_free"
-     {lhss = [\<^term>\<open>(x::i) = y\<close>], proc = K proc};
+fun proc ctxt ct =
+  let
+    val old = Thm.term_of ct
+    val thy = Proof_Context.theory_of ctxt
+    val _ =
+      if Config.get ctxt trace then tracing ("data_free: OLD = " ^ Syntax.string_of_term ctxt old)
+      else ()
+    val (lhs,rhs) = FOLogic.dest_eq old
+    val (lhead, largs) = strip_comb lhs
+    and (rhead, rargs) = strip_comb rhs
+    val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
+    val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
+    val lcon_info = the (Symtab.lookup (ConstructorsData.get thy) lname)
+      handle Option.Option => raise Match;
+    val rcon_info = the (Symtab.lookup (ConstructorsData.get thy) rname)
+      handle Option.Option => raise Match;
+    val new =
+      if #big_rec_name lcon_info = #big_rec_name rcon_info
+          andalso not (null (#free_iffs lcon_info)) then
+        if lname = rname then mk_new (largs, rargs)
+        else \<^Const>\<open>False\<close>
+      else raise Match;
+     val _ =
+       if Config.get ctxt trace then tracing ("NEW = " ^ Syntax.string_of_term ctxt new)
+       else ();
+     val goal = Logic.mk_equals (old, new);
+     val thm = Goal.prove ctxt [] [] goal
+       (fn _ => resolve_tac ctxt @{thms iff_reflection} 1 THEN
+         simp_tac (put_simpset datatype_ss ctxt addsimps
+          (map (Thm.transfer thy) (#free_iffs lcon_info))) 1)
+       handle ERROR msg =>
+       (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal);
+        raise Match)
+  in SOME thm end
+  handle Match => NONE;
 
 end;
 \<close>
 
-setup \<open>
-  Simplifier.map_theory_simpset (fn ctxt => ctxt addsimprocs [DataFree.conv])
-\<close>
+simproc_setup data_free ("(x::i) = y") = \<open>fn _ => Data_Free.proc\<close>
 
 end