src/Pure/axclass.ML

--- a/src/Pure/axclass.ML	Mon Aug 08 22:11:31 2005 +0200
+++ b/src/Pure/axclass.ML	Mon Aug 08 22:14:04 2005 +0200
@@ -319,7 +319,7 @@
 
 fun inst_proof mk_prop add_thms inst int theory =
   theory
-  |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard
+  |> IsarThy.multi_theorem_i Drule.internalK (K I) ProofContext.export_standard
     ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
     (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int;