src/HOL/Tools/specification_package.ML

--- a/src/HOL/Tools/specification_package.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/HOL/Tools/specification_package.ML	Sun May 07 00:22:05 2006 +0200
@@ -231,7 +231,7 @@
     in
       IsarThy.theorem_i PureThy.internalK
         ("", [add_spec axiomatic (zip3 names cnames overloaded), post_proc])
-        (HOLogic.mk_Trueprop ex_prop, ([], [])) thy
+        (HOLogic.mk_Trueprop ex_prop, []) thy
     end