src/HOLCF/Tools/cont_proc.ML

--- a/src/HOLCF/Tools/cont_proc.ML	Thu Jan 22 06:09:41 2009 -0800
+++ b/src/HOLCF/Tools/cont_proc.ML	Thu Jan 22 06:42:05 2009 -0800
@@ -7,7 +7,7 @@
   val is_lcf_term: term -> bool
   val cont_thms: term -> thm list
   val all_cont_thms: term -> thm list
-  val cont_tac: thm list ref -> int -> tactic
+  val cont_tac: int -> tactic
   val cont_proc: theory -> simproc
   val setup: theory -> theory
 end;
@@ -15,15 +15,6 @@
 structure ContProc: CONT_PROC =
 struct
 
-structure ContProcData = TheoryDataFun
-(
-  type T = thm list ref;
-  val empty = ref [];
-  val copy = I;
-  val extend = I;
-  fun merge _ _ = ref [];
-)
-
 (** theory context references **)
 
 val cont_K = @{thm cont_const};
@@ -107,26 +98,21 @@
   conditional rewrite rule with the unsolved subgoals as premises.
 *)
 
-fun cont_tac prev_cont_thms =
+val cont_tac =
   let
     val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
   
-    fun old_cont_tac i thm =
-      case !prev_cont_thms of
-        [] => no_tac thm
-      | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
-
-    fun new_cont_tac f' i thm =
+    fun new_cont_tac f' i =
       case all_cont_thms f' of
-        [] => no_tac thm
-      | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
+        [] => no_tac
+      | (c::cs) => rtac c i;
 
     fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
       let
         val f' = Const (@{const_name Abs_CFun}, dummyT) $ f;
       in
         if is_lcf_term f'
-        then old_cont_tac ORELSE' new_cont_tac f'
+        then new_cont_tac f'
         else REPEAT_ALL_NEW (resolve_tac rules)
       end
       | cont_tac_of_term _ = K no_tac;
@@ -139,8 +125,7 @@
   fun solve_cont thy _ t =
     let
       val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
-      val prev_thms = ContProcData.get thy
-    in Option.map fst (Seq.pull (cont_tac prev_thms 1 tr)) end
+    in Option.map fst (Seq.pull (cont_tac 1 tr)) end
 in
   fun cont_proc thy =
     Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;