implement cont_proc theorem cache using theory data

--- a/src/HOLCF/Tools/cont_proc.ML	Wed Dec 10 13:44:09 2008 -0800
+++ b/src/HOLCF/Tools/cont_proc.ML	Wed Dec 10 15:31:55 2008 -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: int -> tactic
+  val cont_tac: thm list ref -> int -> tactic
   val cont_proc: theory -> simproc
   val setup: theory -> theory
 end;
@@ -15,6 +15,15 @@
 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};
@@ -98,41 +107,40 @@
   conditional rewrite rule with the unsolved subgoals as premises.
 *)
 
-local
-  val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
+fun cont_tac prev_cont_thms =
+  let
+    val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
   
-  (* FIXME proper cache as theory data!? *)
-  val prev_cont_thms : thm list ref = ref [];
+    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 old_cont_tac i thm = CRITICAL (fn () =>
-    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 =
+      case all_cont_thms f' of
+        [] => no_tac thm
+      | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
 
-  fun new_cont_tac f' i thm = CRITICAL (fn () =>
-    case all_cont_thms f' of
-      [] => no_tac thm
-    | (c::cs) => (prev_cont_thms := cs; rtac c i thm));
-
-  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'
-      else REPEAT_ALL_NEW (resolve_tac rules)
-    end
-    | cont_tac_of_term _ = K no_tac;
-in
-  val cont_tac =
-    SUBGOAL (fn (t, i) => cont_tac_of_term (HOLogic.dest_Trueprop t) i);
-end;
+    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'
+        else REPEAT_ALL_NEW (resolve_tac rules)
+      end
+      | cont_tac_of_term _ = K no_tac;
+  in
+    SUBGOAL (fn (t, i) =>
+      cont_tac_of_term (HOLogic.dest_Trueprop t) i)
+  end;
 
 local
   fun solve_cont thy _ t =
     let
       val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
-    in Option.map fst (Seq.pull (cont_tac 1 tr)) end
+      val prev_thms = ContProcData.get thy
+    in Option.map fst (Seq.pull (cont_tac prev_thms 1 tr)) end
 in
   fun cont_proc thy =
     Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;