simplified Proof.theorem(_i) interface;
authorwenzelm
Tue Nov 14 15:29:52 2006 +0100 (2006-11-14)
changeset 21359072e83a0b5bb
parent 21358 f48800c3d573
child 21360 c63755004033
simplified Proof.theorem(_i) interface;
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/specification_package.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/pcpodef_package.ML
src/Pure/Isar/specification.ML
src/Pure/Tools/class_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 14 15:29:50 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 14 15:29:52 2006 +0100
     1.3 @@ -121,7 +121,7 @@
     1.4        val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result
     1.5      in
     1.6        (name, lthy
     1.7 -         |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
     1.8 +         |> Proof.theorem_i PureThy.internalK NONE afterqed [[(goal, [])]]
     1.9           |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd)
    1.10      end
    1.11  
    1.12 @@ -163,8 +163,7 @@
    1.13                                          [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
    1.14          |> set_termination_rule termination
    1.15          |> Proof.theorem_i PureThy.internalK NONE
    1.16 -                           (total_termination_afterqed name data) NONE ("", [])
    1.17 -                           [(("", []), [(goal, [])])]
    1.18 +                           (total_termination_afterqed name data) [[(goal, [])]]
    1.19      end
    1.20  
    1.21  
     2.1 --- a/src/HOL/Tools/specification_package.ML	Tue Nov 14 15:29:50 2006 +0100
     2.2 +++ b/src/HOL/Tools/specification_package.ML	Tue Nov 14 15:29:52 2006 +0100
     2.3 @@ -228,8 +228,7 @@
     2.4      in
     2.5        thy
     2.6        |> ProofContext.init
     2.7 -      |> Proof.theorem_i PureThy.internalK NONE after_qed
     2.8 -        (SOME "") ("", []) [(("", []), [(HOLogic.mk_Trueprop ex_prop, [])])]
     2.9 +      |> Proof.theorem_i PureThy.internalK NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
    2.10      end;
    2.11  
    2.12  
     3.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Nov 14 15:29:50 2006 +0100
     3.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Nov 14 15:29:52 2006 +0100
     3.3 @@ -263,8 +263,7 @@
     3.4      fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th);
     3.5    in
     3.6      ProofContext.init thy
     3.7 -    |> Proof.theorem_i PureThy.internalK NONE after_qed NONE ("", [])
     3.8 -      [(("", []), [(goal, [goal_pat])])]
     3.9 +    |> Proof.theorem_i PureThy.internalK NONE after_qed [[(goal, [goal_pat])]]
    3.10    end;
    3.11  
    3.12  in
     4.1 --- a/src/HOLCF/pcpodef_package.ML	Tue Nov 14 15:29:50 2006 +0100
     4.2 +++ b/src/HOLCF/pcpodef_package.ML	Tue Nov 14 15:29:52 2006 +0100
     4.3 @@ -173,7 +173,7 @@
     4.4      fun after_qed [[th]] = ProofContext.theory (pcpodef_result th);
     4.5    in
     4.6      ProofContext.init thy
     4.7 -    |> Proof.theorem_i PureThy.internalK NONE after_qed NONE ("", []) [(("", []), [(goal, [])])]
     4.8 +    |> Proof.theorem_i PureThy.internalK NONE after_qed [[(goal, [])]]
     4.9    end;
    4.10  
    4.11  fun pcpodef_proof x = gen_pcpodef_proof ProofContext.read_term true x;
     5.1 --- a/src/Pure/Isar/specification.ML	Tue Nov 14 15:29:50 2006 +0100
     5.2 +++ b/src/Pure/Isar/specification.ML	Tue Nov 14 15:29:52 2006 +0100
     5.3 @@ -283,8 +283,7 @@
     5.4        end;
     5.5    in
     5.6      goal_ctxt
     5.7 -    |> Proof.global_goal (K (K ())) Attrib.attribute_i ProofContext.bind_propp_schematic_i
     5.8 -      kind before_qed after_qed' NONE (name, []) stmt
     5.9 +    |> Proof.theorem_i kind before_qed after_qed' (map snd stmt)
    5.10      |> Proof.refine_insert facts
    5.11    end;
    5.12  
     6.1 --- a/src/Pure/Tools/class_package.ML	Tue Nov 14 15:29:50 2006 +0100
     6.2 +++ b/src/Pure/Tools/class_package.ML	Tue Nov 14 15:29:52 2006 +0100
     6.3 @@ -208,8 +208,8 @@
     6.4    in
     6.5      thy
     6.6      |> ProofContext.init
     6.7 -    |> Proof.theorem_i PureThy.internalK NONE after_qed' NONE ("", [])
     6.8 -      ((map (fn t => (("", []), [(t, [])])) o maps (mk_prop thy)) insts)
     6.9 +    |> Proof.theorem_i PureThy.internalK NONE after_qed'
    6.10 +      ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts)
    6.11    end;
    6.12  
    6.13  in