--- a/src/HOL/Tools/recdef_package.ML Tue Nov 21 18:07:29 2006 +0100
+++ b/src/HOL/Tools/recdef_package.ML Tue Nov 21 18:07:30 2006 +0100
@@ -293,7 +293,7 @@
error ("No termination condition #" ^ string_of_int i ^
" in recdef definition of " ^ quote name);
in
- Specification.theorem_i PureThy.internalK NONE (K I) (bname, atts)
+ Specification.theorem_i Thm.internalK NONE (K I) (bname, atts)
[] (Element.Shows [(("", []), [(HOLogic.mk_Trueprop tc, [])])]) lthy
end;
--- a/src/HOL/Tools/specification_package.ML Tue Nov 21 18:07:29 2006 +0100
+++ b/src/HOL/Tools/specification_package.ML Tue Nov 21 18:07:30 2006 +0100
@@ -228,7 +228,7 @@
in
thy
|> ProofContext.init
- |> Proof.theorem_i PureThy.internalK NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
+ |> Proof.theorem_i NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
end;
--- a/src/HOL/Tools/typedef_package.ML Tue Nov 21 18:07:29 2006 +0100
+++ b/src/HOL/Tools/typedef_package.ML Tue Nov 21 18:07:30 2006 +0100
@@ -261,10 +261,7 @@
val (_, goal, goal_pat, typedef_result) =
prepare_typedef prep_term def name typ set opt_morphs thy;
fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th);
- in
- ProofContext.init thy
- |> Proof.theorem_i PureThy.internalK NONE after_qed [[(goal, [goal_pat])]]
- end;
+ in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] (ProofContext.init thy) end;
in
--- a/src/HOLCF/pcpodef_package.ML Tue Nov 21 18:07:29 2006 +0100
+++ b/src/HOLCF/pcpodef_package.ML Tue Nov 21 18:07:30 2006 +0100
@@ -171,10 +171,7 @@
val (goal, pcpodef_result) =
prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
fun after_qed [[th]] = ProofContext.theory (pcpodef_result th);
- in
- ProofContext.init thy
- |> Proof.theorem_i PureThy.internalK NONE after_qed [[(goal, [])]]
- end;
+ in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end;
fun pcpodef_proof x = gen_pcpodef_proof ProofContext.read_term true x;
fun pcpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term true x;