--- a/src/HOLCF/Cont.thy Thu Apr 30 12:16:35 2009 -0700
+++ b/src/HOLCF/Cont.thy Thu Apr 30 14:46:59 2009 -0700
@@ -144,7 +144,7 @@
( val name = "cont2cont" val description = "continuity intro rule" )
*}
-setup {* Cont2ContData.setup *}
+setup Cont2ContData.setup
text {*
Given the term @{term "cont f"}, the procedure tries to construct the
@@ -153,20 +153,13 @@
conditional rewrite rule with the unsolved subgoals as premises.
*}
-setup {*
-let
- fun solve_cont thy ss t =
+simproc_setup cont_proc ("cont f") = {*
+ fn phi => fn ss => fn ct =>
let
- val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
+ val tr = instantiate' [] [SOME ct] @{thm Eq_TrueI};
val rules = Cont2ContData.get (Simplifier.the_context ss);
val tac = REPEAT_ALL_NEW (match_tac rules);
- in Option.map fst (Seq.pull (tac 1 tr)) end
-
- val proc =
- Simplifier.simproc @{theory} "cont_proc" ["cont f"] solve_cont;
-in
- Simplifier.map_simpset (fn ss => ss addsimprocs [proc])
-end
+ in SINGLE (tac 1) tr end
*}
subsection {* Continuity of basic functions *}