src/HOL/Tools/specification_package.ML

--- a/src/HOL/Tools/specification_package.ML	Tue Nov 14 15:29:50 2006 +0100
+++ b/src/HOL/Tools/specification_package.ML	Tue Nov 14 15:29:52 2006 +0100
@@ -228,8 +228,7 @@
     in
       thy
       |> ProofContext.init
-      |> Proof.theorem_i PureThy.internalK NONE after_qed
-        (SOME "") ("", []) [(("", []), [(HOLogic.mk_Trueprop ex_prop, [])])]
+      |> Proof.theorem_i PureThy.internalK NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
     end;