author wenzelm Mon, 16 Jun 2008 17:54:46 +0200 changeset 27232 7cd256da0a36 parent 27231 ef7cc91a0d7f child 27233 224c830e7abe
```--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Jun 16 17:54:45 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Jun 16 17:54:46 2008 +0200
@@ -603,6 +603,8 @@

fun comp_theorems (comp_dnam, eqs: eq list) thy =
let
+val global_ctxt = ProofContext.init thy;
+
val dnames = map (fst o fst) eqs;
val conss  = map  snd        eqs;
val comp_dname = Sign.full_name thy comp_dnam;
@@ -687,7 +689,7 @@
in pg copy_take_defs goal tacs end;
in
val take_rews = map standard
-    (atomize take_stricts @ take_0s @ atomize take_apps);
+    (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
end; (* local *)

local
@@ -864,7 +866,7 @@
fast_tac HOL_cs 1];
in pg axs_finite_def goal tacs end;

-        val finites = map one_finite (dnames ~~ atomize finite_lemma1b);
+        val finites = map one_finite (dnames ~~ atomize global_ctxt finite_lemma1b);
val ind =
let
fun concf n dn = %:(P_name n) \$ %:(x_name n);
@@ -877,7 +879,7 @@
ind_prems_tac prems];
in
TRY (safe_tac HOL_cs) ::
-                maps finite_tacs (finites ~~ atomize finite_ind)
+                maps finite_tacs (finites ~~ atomize global_ctxt finite_ind)
end;
in pg'' thy [] (ind_term concf) tacf end;
in (finites, ind) end (* let *)
@@ -885,8 +887,8 @@
else (* infinite case *)
let
fun one_finite n dn =