src/Pure/Tools/class_package.ML

--- a/src/Pure/Tools/class_package.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Sun May 07 00:22:05 2006 +0200
@@ -301,7 +301,7 @@
   thy
   |> ProofContext.init
   |> Proof.theorem_i PureThy.internalK NONE (after_qed oo (fold o fold) add_thm) NONE ("", [])
-       (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
+       (map (fn t => (("", []), [(t, [])])) (mk_prop thy inst));
 
 in