# HG changeset patch
# User wenzelm
# Date 1697574348 -7200
# Node ID 2cb027b951886013fdef38aba00aa1f26bee05d3
# Parent  103467dc5117ff8dfdde04786fad2f35f1123c08
clarified 'simproc_setup';

diff -r 103467dc5117 -r 2cb027b95188 src/HOL/HOLCF/Domain_Aux.thy
--- a/src/HOL/HOLCF/Domain_Aux.thy	Tue Oct 17 18:55:29 2023 +0200
+++ b/src/HOL/HOLCF/Domain_Aux.thy	Tue Oct 17 22:25:48 2023 +0200
@@ -358,6 +358,8 @@
 ML_file \<open>Tools/Domain/domain_take_proofs.ML\<close>
 ML_file \<open>Tools/cont_consts.ML\<close>
 ML_file \<open>Tools/cont_proc.ML\<close>
+simproc_setup cont ("cont f") = \<open>K ContProc.cont_proc\<close>
+
 ML_file \<open>Tools/Domain/domain_constructors.ML\<close>
 ML_file \<open>Tools/Domain/domain_induction.ML\<close>
 
diff -r 103467dc5117 -r 2cb027b95188 src/HOL/HOLCF/Tools/cont_proc.ML
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Tue Oct 17 18:55:29 2023 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Tue Oct 17 22:25:48 2023 +0200
@@ -8,8 +8,7 @@
   val cont_thms: term -> thm list
   val all_cont_thms: term -> thm list
   val cont_tac: Proof.context -> int -> tactic
-  val cont_proc: simproc
-  val setup: theory -> theory
+  val cont_proc: Proof.context -> cterm -> thm option
 end
 
 structure ContProc : CONT_PROC =
@@ -115,18 +114,10 @@
       cont_tac_of_term (HOLogic.dest_Trueprop t) i)
   end
 
-local
-  fun solve_cont ctxt ct =
-    let
-      val t = Thm.term_of ct
-      val tr = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
-    in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end
-in
-  val cont_proc =
-    Simplifier.make_simproc \<^context> "cont_proc"
-     {lhss = [\<^term>\<open>cont f\<close>], proc = K solve_cont}
-end
-
-val setup = map_theory_simpset (fn ctxt => ctxt addsimprocs [cont_proc])
+fun cont_proc ctxt ct =
+  let
+    val t = Thm.term_of ct
+    val tr = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
+  in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end
 
 end