# HG changeset patch
# User wenzelm
# Date 1163514592 -3600
# Node ID 072e83a0b5bbd91c81b5396b699d4b1e01165b82
# Parent  f48800c3d573f229405466548f50eb28d31916fb
simplified Proof.theorem(_i) interface;

diff -r f48800c3d573 -r 072e83a0b5bb src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 14 15:29:50 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 14 15:29:52 2006 +0100
@@ -121,7 +121,7 @@
       val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result
     in
       (name, lthy
-         |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
+         |> Proof.theorem_i PureThy.internalK NONE afterqed [[(goal, [])]]
          |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd)
     end
 
@@ -163,8 +163,7 @@
                                         [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
         |> set_termination_rule termination
         |> Proof.theorem_i PureThy.internalK NONE
-                           (total_termination_afterqed name data) NONE ("", [])
-                           [(("", []), [(goal, [])])]
+                           (total_termination_afterqed name data) [[(goal, [])]]
     end
 
 
diff -r f48800c3d573 -r 072e83a0b5bb src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Tue Nov 14 15:29:50 2006 +0100
+++ b/src/HOL/Tools/specification_package.ML	Tue Nov 14 15:29:52 2006 +0100
@@ -228,8 +228,7 @@
     in
       thy
       |> ProofContext.init
-      |> Proof.theorem_i PureThy.internalK NONE after_qed
-        (SOME "") ("", []) [(("", []), [(HOLogic.mk_Trueprop ex_prop, [])])]
+      |> Proof.theorem_i PureThy.internalK NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
     end;
 
 
diff -r f48800c3d573 -r 072e83a0b5bb src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Tue Nov 14 15:29:50 2006 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Tue Nov 14 15:29:52 2006 +0100
@@ -263,8 +263,7 @@
     fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th);
   in
     ProofContext.init thy
-    |> Proof.theorem_i PureThy.internalK NONE after_qed NONE ("", [])
-      [(("", []), [(goal, [goal_pat])])]
+    |> Proof.theorem_i PureThy.internalK NONE after_qed [[(goal, [goal_pat])]]
   end;
 
 in
diff -r f48800c3d573 -r 072e83a0b5bb src/HOLCF/pcpodef_package.ML
--- a/src/HOLCF/pcpodef_package.ML	Tue Nov 14 15:29:50 2006 +0100
+++ b/src/HOLCF/pcpodef_package.ML	Tue Nov 14 15:29:52 2006 +0100
@@ -173,7 +173,7 @@
     fun after_qed [[th]] = ProofContext.theory (pcpodef_result th);
   in
     ProofContext.init thy
-    |> Proof.theorem_i PureThy.internalK NONE after_qed NONE ("", []) [(("", []), [(goal, [])])]
+    |> Proof.theorem_i PureThy.internalK NONE after_qed [[(goal, [])]]
   end;
 
 fun pcpodef_proof x = gen_pcpodef_proof ProofContext.read_term true x;
diff -r f48800c3d573 -r 072e83a0b5bb src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Nov 14 15:29:50 2006 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Nov 14 15:29:52 2006 +0100
@@ -283,8 +283,7 @@
       end;
   in
     goal_ctxt
-    |> Proof.global_goal (K (K ())) Attrib.attribute_i ProofContext.bind_propp_schematic_i
-      kind before_qed after_qed' NONE (name, []) stmt
+    |> Proof.theorem_i kind before_qed after_qed' (map snd stmt)
     |> Proof.refine_insert facts
   end;
 
diff -r f48800c3d573 -r 072e83a0b5bb src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Tue Nov 14 15:29:50 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Tue Nov 14 15:29:52 2006 +0100
@@ -208,8 +208,8 @@
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i PureThy.internalK NONE after_qed' NONE ("", [])
-      ((map (fn t => (("", []), [(t, [])])) o maps (mk_prop thy)) insts)
+    |> Proof.theorem_i PureThy.internalK NONE after_qed'
+      ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts)
   end;
 
 in