changeset 11740 | 86ac4189a1c1 |
parent 11541 | 09dc5e8ac99c |
child 11828 | ef3e51b1b4ec |
--- a/src/Pure/axclass.ML Sat Oct 13 20:31:05 2001 +0200 +++ b/src/Pure/axclass.ML Sat Oct 13 20:31:34 2001 +0200 @@ -440,7 +440,7 @@ fun inst_proof mk_prop add_thms (sig_prop, comment) int thy = thy - |> IsarThy.theorem_i ((("", [inst_attribute add_thms]), + |> IsarThy.theorem_i Drule.internalK ((("", [inst_attribute add_thms]), (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int; val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;