# HG changeset patch
# User huffman
# Date 1241128019 25200
# Node ID 5ee6368d622bdbc6ee577e0c33625667ee774886
# Parent  e564767f8f78066b1066460106ea7f6e37048dc6
use simproc_setup command for cont_proc

diff -r e564767f8f78 -r 5ee6368d622b src/HOLCF/Cont.thy
--- 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 *}