1.1 --- a/src/HOLCF/Cont.thy	Thu Apr 30 12:16:35 2009 -0700
     1.2 +++ b/src/HOLCF/Cont.thy	Thu Apr 30 14:46:59 2009 -0700
     1.3 @@ -144,7 +144,7 @@
     1.4    ( val name = "cont2cont" val description = "continuity intro rule" )
     1.5  *}
     1.6  
     1.7 -setup {* Cont2ContData.setup *}
     1.8 +setup Cont2ContData.setup
     1.9  
    1.10  text {*
    1.11    Given the term @{term "cont f"}, the procedure tries to construct the
    1.12 @@ -153,20 +153,13 @@
    1.13    conditional rewrite rule with the unsolved subgoals as premises.
    1.14  *}
    1.15  
    1.16 -setup {*
    1.17 -let
    1.18 -  fun solve_cont thy ss t =
    1.19 +simproc_setup cont_proc ("cont f") = {*
    1.20 +  fn phi => fn ss => fn ct =>
    1.21      let
    1.22 -      val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
    1.23 +      val tr = instantiate' [] [SOME ct] @{thm Eq_TrueI};
    1.24        val rules = Cont2ContData.get (Simplifier.the_context ss);
    1.25        val tac = REPEAT_ALL_NEW (match_tac rules);
    1.26 -    in Option.map fst (Seq.pull (tac 1 tr)) end
    1.27 -
    1.28 -  val proc =
    1.29 -    Simplifier.simproc @{theory} "cont_proc" ["cont f"] solve_cont;
    1.30 -in
    1.31 -  Simplifier.map_simpset (fn ss => ss addsimprocs [proc])
    1.32 -end
    1.33 +    in SINGLE (tac 1) tr end
    1.34  *}
    1.35  
    1.36  subsection {* Continuity of basic functions *}