src/Pure/Isar/local_defs.ML

--- a/src/Pure/Isar/local_defs.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sun May 07 00:22:05 2006 +0200
@@ -84,7 +84,7 @@
   in
     ctxt
     |> ProofContext.add_fixes_i [(x, NONE, NoSyn)] |> snd
-    |> ProofContext.add_assms_i def_export [(("", []), [(eq, ([], []))])]
+    |> ProofContext.add_assms_i def_export [(("", []), [(eq, [])])]
     |>> (fn [(_, [th])] => (x', th))
   end;