src/Pure/axclass.ML

--- a/src/Pure/axclass.ML	Tue Nov 08 10:43:15 2005 +0100
+++ b/src/Pure/axclass.ML	Tue Nov 08 10:44:40 2005 +0100
@@ -303,7 +303,7 @@
 
 fun gen_instance mk_prop add_thms inst thy = thy
   |> ProofContext.init
-  |> Proof.theorem_i Drule.internalK NONE (K (fold add_thms)) NONE ("", [])
+  |> Proof.theorem_i Drule.internalK NONE (fold add_thms) NONE ("", [])
     (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
 
 in