--- a/src/HOL/Tools/recdef_package.ML Thu Jan 10 01:10:58 2002 +0100
+++ b/src/HOL/Tools/recdef_package.ML Thu Jan 10 01:11:43 2002 +0100
@@ -311,7 +311,7 @@
error ("No termination condition #" ^ string_of_int i ^
" in recdef definition of " ^ quote name);
in
- thy |> IsarThy.theorem_i Drule.internalK (None, [])
+ thy |> IsarThy.theorem_i Drule.internalK
(((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int
end;
--- a/src/HOL/Tools/typedef_package.ML Thu Jan 10 01:10:58 2002 +0100
+++ b/src/HOL/Tools/typedef_package.ML Thu Jan 10 01:11:43 2002 +0100
@@ -247,8 +247,8 @@
prepare_typedef prep_term true name typ set opt_morphs thy;
val att = #1 o att_result;
in
- thy |> IsarThy.theorem_i Drule.internalK (None, [])
- ((("", [att]), (goal, ([goal_pat], []))), comment) int
+ thy
+ |> IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
end;
val typedef_proof = gen_typedef_proof read_term;
--- a/src/Pure/axclass.ML Thu Jan 10 01:10:58 2002 +0100
+++ b/src/Pure/axclass.ML Thu Jan 10 01:11:43 2002 +0100
@@ -423,7 +423,7 @@
fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
thy
- |> IsarThy.theorem_i Drule.internalK (None, []) ((("", [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;