1.1 --- a/src/HOL/Tools/typedef_package.ML Mon Nov 13 10:34:32 2000 +0100
1.2 +++ b/src/HOL/Tools/typedef_package.ML Mon Nov 13 21:59:49 2000 +0100
1.3 @@ -239,7 +239,7 @@
1.4 val goal_pat = Thm.term_of (goal_nonempty true cset_pat);
1.5 in
1.6 thy
1.7 - |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef],
1.8 + |> IsarThy.theorem_i ((("", [typedef_attribute cset do_typedef]),
1.9 (goal, ([goal_pat], []))), comment) int
1.10 end;
1.11
2.1 --- a/src/Pure/axclass.ML Mon Nov 13 10:34:32 2000 +0100
2.2 +++ b/src/Pure/axclass.ML Mon Nov 13 21:59:49 2000 +0100
2.3 @@ -439,7 +439,7 @@
2.4
2.5 fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
2.6 thy
2.7 - |> IsarThy.theorem_i (("", [inst_attribute add_thms],
2.8 + |> IsarThy.theorem_i ((("", [inst_attribute add_thms]),
2.9 (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
2.10
2.11 val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;