src/Pure/axclass.ML
changeset 15596 8665d08085df
parent 15570 8d8c70b41bab
child 15696 1da4ce092c0b
     1.1 --- a/src/Pure/axclass.ML	Tue Mar 08 16:02:52 2005 +0100
     1.2 +++ b/src/Pure/axclass.ML	Wed Mar 09 18:44:52 2005 +0100
     1.3 @@ -407,7 +407,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
     1.8 +  |> IsarThy.multi_theorem_i Drule.internalK I
     1.9      ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
    1.10      (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;
    1.11