src/Pure/axclass.ML
changeset 12694 9950c1ce9d24
parent 12493 de2575b6cd38
child 12876 a70df1e5bf10
     1.1 --- a/src/Pure/axclass.ML	Thu Jan 10 01:10:58 2002 +0100
     1.2 +++ b/src/Pure/axclass.ML	Thu Jan 10 01:11:43 2002 +0100
     1.3 @@ -423,7 +423,7 @@
     1.4  
     1.5  fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
     1.6    thy
     1.7 -  |> IsarThy.theorem_i Drule.internalK (None, []) ((("", [inst_attribute add_thms]),
     1.8 +  |> IsarThy.theorem_i Drule.internalK ((("", [inst_attribute add_thms]),
     1.9      (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
    1.10  
    1.11  val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;