diff -r dc8a41c7cefc -r 8665d08085df src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Mar 08 16:02:52 2005 +0100
+++ b/src/Pure/axclass.ML	Wed Mar 09 18:44:52 2005 +0100
@@ -407,7 +407,7 @@
 
 fun inst_proof mk_prop add_thms inst int theory =
   theory
-  |> IsarThy.multi_theorem_i Drule.internalK
+  |> IsarThy.multi_theorem_i Drule.internalK I
     ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
     (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;