src/Pure/axclass.ML
changeset 6935 a3f3f4128cab
parent 6729 b6e167580a32
child 7351 1e485129fbc1
     1.1 --- a/src/Pure/axclass.ML	Thu Jul 08 18:35:44 1999 +0200
     1.2 +++ b/src/Pure/axclass.ML	Thu Jul 08 18:36:09 1999 +0200
     1.3 @@ -408,7 +408,7 @@
     1.4  fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
     1.5    thy
     1.6    |> IsarThy.theorem_i (("", [inst_attribute add_thms],
     1.7 -    (mk_prop (Theory.sign_of thy) sig_prop, [])), comment) int;
     1.8 +    (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
     1.9  
    1.10  val instance_subclass_proof = inst_proof (mk_classrel oo intrn_classrel) add_classrel_thms;
    1.11  val instance_subclass_proof_i = inst_proof (K mk_classrel) add_classrel_thms;