src/HOLCF/pcpodef_package.ML

--- a/src/HOLCF/pcpodef_package.ML	Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOLCF/pcpodef_package.ML	Sat Jan 21 23:02:14 2006 +0100
@@ -144,8 +144,9 @@
           ||> Theory.parent_path;
       in (theory', defs) end;
     
-    fun pcpodef_result (theory, UUmem_admissible) =
+    fun pcpodef_result (context, UUmem_admissible) =
       let
+        val theory = Context.the_theory context;
         val UUmem = UUmem_admissible RS conjunct1;
         val admissible = UUmem_admissible RS conjunct2;
       in
@@ -153,18 +154,19 @@
         |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1)
         |> make_cpo admissible
         |> make_pcpo UUmem
-        |> (fn (theory', (type_def, _, _)) => (theory', type_def))
+        |> (fn (theory', (type_def, _, _)) => (Context.Theory theory', type_def))
       end;
   
-    fun cpodef_result (theory, nonempty_admissible) =
+    fun cpodef_result (context, nonempty_admissible) =
       let
+        val theory = Context.the_theory context;
         val nonempty = nonempty_admissible RS conjunct1;
         val admissible = nonempty_admissible RS conjunct2;
       in
         theory
         |> make_po (Tactic.rtac nonempty 1)
         |> make_cpo admissible
-        |> (fn (theory', (type_def, _, _)) => (theory', type_def))
+        |> (fn (theory', (type_def, _, _)) => (Context.Theory theory', type_def))
       end;
   
   in (goal, if pcpo then pcpodef_result else cpodef_result) end