src/HOLCF/pcpodef_package.ML

--- a/src/HOLCF/pcpodef_package.ML	Tue Nov 14 15:29:50 2006 +0100
+++ b/src/HOLCF/pcpodef_package.ML	Tue Nov 14 15:29:52 2006 +0100
@@ -173,7 +173,7 @@
     fun after_qed [[th]] = ProofContext.theory (pcpodef_result th);
   in
     ProofContext.init thy
-    |> Proof.theorem_i PureThy.internalK NONE after_qed NONE ("", []) [(("", []), [(goal, [])])]
+    |> Proof.theorem_i PureThy.internalK NONE after_qed [[(goal, [])]]
   end;
 
 fun pcpodef_proof x = gen_pcpodef_proof ProofContext.read_term true x;