# HG changeset patch
# User wenzelm
# Date 1164128850 -3600
# Node ID 944f80576be09f256374751b754b76f36490e696
# Parent  89104dca628efeed56d8973cca4c04c70c8bc3d0
simplified Proof.theorem(_i);

diff -r 89104dca628e -r 944f80576be0 src/HOL/Tools/recdef_package.ML
--- 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;
 
diff -r 89104dca628e -r 944f80576be0 src/HOL/Tools/specification_package.ML
--- 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;
 
 
diff -r 89104dca628e -r 944f80576be0 src/HOL/Tools/typedef_package.ML
--- 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
 
diff -r 89104dca628e -r 944f80576be0 src/HOLCF/pcpodef_package.ML
--- 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;