src/Pure/axclass.ML
changeset 17034 b4d9b87c102e
parent 16486 1a12cdb6ee6b
child 17041 dee6f7047cae
     1.1 --- a/src/Pure/axclass.ML	Mon Aug 08 22:11:31 2005 +0200
     1.2 +++ b/src/Pure/axclass.ML	Mon Aug 08 22:14:04 2005 +0200
     1.3 @@ -319,7 +319,7 @@
     1.4  
     1.5  fun inst_proof mk_prop add_thms inst int theory =
     1.6    theory
     1.7 -  |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard
     1.8 +  |> IsarThy.multi_theorem_i Drule.internalK (K I) ProofContext.export_standard
     1.9      ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
    1.10      (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int;
    1.11