simplified method setup;
authorwenzelm
Wed Nov 29 15:44:51 2006 +0100 (2006-11-29)
changeset 21588cd0dc678a205
parent 21587 a3561bfe0ada
child 21589 1b02201d7195
simplified method setup;
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/ringsimp.ML
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/OtwayReesBella.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/Smartcard/ShoupRubin.thy
src/HOL/Auth/Smartcard/ShoupRubinBella.thy
src/HOL/Auth/Smartcard/Smartcard.thy
src/HOL/Hoare/Hoare.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/HoareParallel/OG_Tactics.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/transfer.ML
src/HOL/Import/shuffler.ML
src/HOL/Integ/presburger.ML
src/HOL/Isar_examples/Hoare.thy
src/HOL/Library/comm_ring.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Prolog/HOHH.thy
src/HOL/Real/ferrante_rackoff.ML
src/HOL/SAT.thy
src/HOL/SET-Protocol/EventSET.thy
src/HOL/SET-Protocol/MessageSET.thy
src/HOL/SET-Protocol/PublicSET.thy
src/HOL/Tools/Presburger/presburger.ML
src/HOL/Tools/function_package/auto_term.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/UNITY/Simple/NSP_Bad.thy
src/HOL/UNITY/UNITY_Main.thy
src/HOL/ex/Reflection.thy
src/HOL/ex/SAT_Examples.thy
src/Provers/eqsubst.ML
src/Provers/hypsubst.ML
src/Provers/splitter.ML
src/Sequents/ILL.thy
src/Sequents/LK0.thy
src/ZF/UNITY/Constrains.thy
     1.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Nov 29 15:44:46 2006 +0100
     1.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Nov 29 15:44:51 2006 +0100
     1.3 @@ -231,7 +231,7 @@
     1.4  *}   (* Note: r_one is not necessary in ring_ss *)
     1.5  
     1.6  method_setup ring =
     1.7 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *}
     1.8 +  {* Method.no_args (Method.SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
     1.9    {* computes distributive normal form in rings *}
    1.10  
    1.11  lemmas ring_simps =
     2.1 --- a/src/HOL/Algebra/ringsimp.ML	Wed Nov 29 15:44:46 2006 +0100
     2.2 +++ b/src/HOL/Algebra/ringsimp.ML	Wed Nov 29 15:44:51 2006 +0100
     2.3 @@ -60,9 +60,6 @@
     2.4  fun algebra_tac ctxt =
     2.5    EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt)));
     2.6  
     2.7 -val method =
     2.8 -  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' HEADGOAL (algebra_tac ctxt))
     2.9 -
    2.10  
    2.11  (** Attribute **)
    2.12  
    2.13 @@ -87,8 +84,8 @@
    2.14  
    2.15  val setup =
    2.16    AlgebraData.init #>
    2.17 -  Method.add_methods [("algebra", method, "normalisation of algebraic structure")] #>
    2.18 +  Method.add_methods [("algebra", Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac),
    2.19 +    "normalisation of algebraic structure")] #>
    2.20    Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
    2.21  
    2.22 -
    2.23  end;
     3.1 --- a/src/HOL/Auth/Event.thy	Wed Nov 29 15:44:46 2006 +0100
     3.2 +++ b/src/HOL/Auth/Event.thy	Wed Nov 29 15:44:51 2006 +0100
     3.3 @@ -290,8 +290,7 @@
     3.4      intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
     3.5  
     3.6  method_setup analz_mono_contra = {*
     3.7 -    Method.no_args
     3.8 -      (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
     3.9 +    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
    3.10      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
    3.11  
    3.12  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
    3.13 @@ -349,8 +348,7 @@
    3.14  *}
    3.15  
    3.16  method_setup synth_analz_mono_contra = {*
    3.17 -    Method.no_args
    3.18 -      (Method.METHOD (fn facts => REPEAT_FIRST synth_analz_mono_contra_tac)) *}
    3.19 +    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
    3.20      "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
    3.21  
    3.22  end
     4.1 --- a/src/HOL/Auth/Message.thy	Wed Nov 29 15:44:46 2006 +0100
     4.2 +++ b/src/HOL/Auth/Message.thy	Wed Nov 29 15:44:51 2006 +0100
     4.3 @@ -948,20 +948,17 @@
     4.4  
     4.5  method_setup spy_analz = {*
     4.6      Method.ctxt_args (fn ctxt =>
     4.7 -        Method.METHOD (fn facts => 
     4.8 -            gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
     4.9 +        Method.SIMPLE_METHOD (gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    4.10      "for proving the Fake case when analz is involved"
    4.11  
    4.12  method_setup atomic_spy_analz = {*
    4.13      Method.ctxt_args (fn ctxt =>
    4.14 -        Method.METHOD (fn facts => 
    4.15 -            atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    4.16 +        Method.SIMPLE_METHOD (atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    4.17      "for debugging spy_analz"
    4.18  
    4.19  method_setup Fake_insert_simp = {*
    4.20      Method.ctxt_args (fn ctxt =>
    4.21 -        Method.METHOD (fn facts =>
    4.22 -            Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
    4.23 +        Method.SIMPLE_METHOD (Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
    4.24      "for debugging spy_analz"
    4.25  
    4.26  
     5.1 --- a/src/HOL/Auth/OtwayReesBella.thy	Wed Nov 29 15:44:46 2006 +0100
     5.2 +++ b/src/HOL/Auth/OtwayReesBella.thy	Wed Nov 29 15:44:51 2006 +0100
     5.3 @@ -142,9 +142,7 @@
     5.4  *}
     5.5   
     5.6  method_setup parts_explicit = {*
     5.7 -    Method.ctxt_args (fn ctxt =>
     5.8 -        Method.METHOD (fn facts =>
     5.9 -            parts_explicit_tac 1)) *}
    5.10 +    Method.no_args (Method.SIMPLE_METHOD' parts_explicit_tac) *}
    5.11    "to explicitly state that some message components belong to parts knows Spy"
    5.12  
    5.13  
    5.14 @@ -263,8 +261,8 @@
    5.15  
    5.16  method_setup analz_freshCryptK = {*
    5.17      Method.ctxt_args (fn ctxt =>
    5.18 -     (Method.METHOD
    5.19 -      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    5.20 +     (Method.SIMPLE_METHOD
    5.21 +      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    5.22                            REPEAT_FIRST (rtac analz_image_freshCryptK_lemma),
    5.23                            ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
    5.24    "for proving useful rewrite rule"
    5.25 @@ -272,8 +270,8 @@
    5.26  
    5.27  method_setup disentangle = {*
    5.28      Method.no_args
    5.29 -     (Method.METHOD
    5.30 -      (fn facts => REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
    5.31 +     (Method.SIMPLE_METHOD
    5.32 +      (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
    5.33                     ORELSE' hyp_subst_tac))) *}
    5.34    "for eliminating conjunctions, disjunctions and the like"
    5.35  
     6.1 --- a/src/HOL/Auth/Public.thy	Wed Nov 29 15:44:46 2006 +0100
     6.2 +++ b/src/HOL/Auth/Public.thy	Wed Nov 29 15:44:51 2006 +0100
     6.3 @@ -415,8 +415,8 @@
     6.4  
     6.5  method_setup analz_freshK = {*
     6.6      Method.ctxt_args (fn ctxt =>
     6.7 -     (Method.METHOD
     6.8 -      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
     6.9 +     (Method.SIMPLE_METHOD
    6.10 +      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    6.11                            REPEAT_FIRST (rtac analz_image_freshK_lemma),
    6.12                            ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
    6.13      "for proving the Session Key Compromise theorem"
    6.14 @@ -449,8 +449,7 @@
    6.15  
    6.16  method_setup possibility = {*
    6.17      Method.ctxt_args (fn ctxt =>
    6.18 -        Method.METHOD (fn facts =>
    6.19 -            gen_possibility_tac (local_simpset_of ctxt))) *}
    6.20 +        Method.SIMPLE_METHOD (gen_possibility_tac (local_simpset_of ctxt))) *}
    6.21      "for proving possibility theorems"
    6.22  
    6.23  end
     7.1 --- a/src/HOL/Auth/Shared.thy	Wed Nov 29 15:44:46 2006 +0100
     7.2 +++ b/src/HOL/Auth/Shared.thy	Wed Nov 29 15:44:51 2006 +0100
     7.3 @@ -265,16 +265,15 @@
     7.4  
     7.5  method_setup analz_freshK = {*
     7.6      Method.ctxt_args (fn ctxt =>
     7.7 -     (Method.METHOD
     7.8 -      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
     7.9 +     (Method.SIMPLE_METHOD
    7.10 +      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    7.11                            REPEAT_FIRST (rtac analz_image_freshK_lemma),
    7.12                            ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
    7.13      "for proving the Session Key Compromise theorem"
    7.14  
    7.15  method_setup possibility = {*
    7.16      Method.ctxt_args (fn ctxt =>
    7.17 -        Method.METHOD (fn facts =>
    7.18 -            gen_possibility_tac (local_simpset_of ctxt))) *}
    7.19 +        Method.SIMPLE_METHOD (gen_possibility_tac (local_simpset_of ctxt))) *}
    7.20      "for proving possibility theorems"
    7.21  
    7.22  lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
     8.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Wed Nov 29 15:44:46 2006 +0100
     8.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Wed Nov 29 15:44:51 2006 +0100
     8.3 @@ -774,15 +774,15 @@
     8.4  *}
     8.5  
     8.6  method_setup prepare = {*
     8.7 -    Method.no_args (Method.METHOD (fn facts => prepare_tac)) *}
     8.8 +    Method.no_args (Method.SIMPLE_METHOD prepare_tac) *}
     8.9    "to launch a few simple facts that'll help the simplifier"
    8.10  
    8.11  method_setup parts_prepare = {*
    8.12 -    Method.no_args (Method.METHOD (fn facts => parts_prepare_tac)) *}
    8.13 +    Method.no_args (Method.SIMPLE_METHOD parts_prepare_tac) *}
    8.14    "additional facts to reason about parts"
    8.15  
    8.16  method_setup analz_prepare = {*
    8.17 -    Method.no_args (Method.METHOD (fn facts => analz_prepare_tac)) *}
    8.18 +    Method.no_args (Method.SIMPLE_METHOD analz_prepare_tac) *}
    8.19    "additional facts to reason about analz"
    8.20  
    8.21  
    8.22 @@ -836,8 +836,8 @@
    8.23  
    8.24  method_setup sc_analz_freshK = {*
    8.25      Method.ctxt_args (fn ctxt =>
    8.26 -     (Method.METHOD
    8.27 -      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    8.28 +     (Method.SIMPLE_METHOD
    8.29 +      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    8.30                            REPEAT_FIRST (rtac analz_image_freshK_lemma),
    8.31                            ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss
    8.32                                      addsimps [knows_Spy_Inputs_secureM_sr_Spy,
     9.1 --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Wed Nov 29 15:44:46 2006 +0100
     9.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Wed Nov 29 15:44:51 2006 +0100
     9.3 @@ -782,15 +782,15 @@
     9.4  *}
     9.5  
     9.6  method_setup prepare = {*
     9.7 -    Method.no_args (Method.METHOD (fn facts => prepare_tac)) *}
     9.8 +    Method.no_args (Method.SIMPLE_METHOD prepare_tac) *}
     9.9    "to launch a few simple facts that'll help the simplifier"
    9.10  
    9.11  method_setup parts_prepare = {*
    9.12 -    Method.no_args (Method.METHOD (fn facts => parts_prepare_tac)) *}
    9.13 +    Method.no_args (Method.SIMPLE_METHOD parts_prepare_tac) *}
    9.14    "additional facts to reason about parts"
    9.15  
    9.16  method_setup analz_prepare = {*
    9.17 -    Method.no_args (Method.METHOD (fn facts => analz_prepare_tac)) *}
    9.18 +    Method.no_args (Method.SIMPLE_METHOD analz_prepare_tac) *}
    9.19    "additional facts to reason about analz"
    9.20  
    9.21  
    9.22 @@ -845,8 +845,8 @@
    9.23  
    9.24  method_setup sc_analz_freshK = {*
    9.25      Method.ctxt_args (fn ctxt =>
    9.26 -     (Method.METHOD
    9.27 -      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    9.28 +     (Method.SIMPLE_METHOD
    9.29 +      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    9.30                            REPEAT_FIRST (rtac analz_image_freshK_lemma),
    9.31                            ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss
    9.32                                      addsimps [knows_Spy_Inputs_secureM_srb_Spy,
    10.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Nov 29 15:44:46 2006 +0100
    10.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Nov 29 15:44:51 2006 +0100
    10.3 @@ -442,16 +442,15 @@
    10.4  
    10.5  method_setup analz_freshK = {*
    10.6      Method.ctxt_args (fn ctxt =>
    10.7 -     (Method.METHOD
    10.8 -      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    10.9 +     (Method.SIMPLE_METHOD
   10.10 +      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   10.11                            REPEAT_FIRST (rtac analz_image_freshK_lemma),
   10.12                            ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
   10.13      "for proving the Session Key Compromise theorem"
   10.14  
   10.15  method_setup possibility = {*
   10.16      Method.ctxt_args (fn ctxt =>
   10.17 -        Method.METHOD (fn facts =>
   10.18 -            gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
   10.19 +        Method.SIMPLE_METHOD (gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
   10.20      "for proving possibility theorems"
   10.21  
   10.22  lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
    11.1 --- a/src/HOL/Hoare/Hoare.thy	Wed Nov 29 15:44:46 2006 +0100
    11.2 +++ b/src/HOL/Hoare/Hoare.thy	Wed Nov 29 15:44:51 2006 +0100
    11.3 @@ -228,14 +228,12 @@
    11.4  use "hoare.ML"
    11.5  
    11.6  method_setup vcg = {*
    11.7 -  Method.no_args
    11.8 -    (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
    11.9 +  Method.no_args (Method.SIMPLE_METHOD' (hoare_tac (K all_tac))) *}
   11.10    "verification condition generator"
   11.11  
   11.12  method_setup vcg_simp = {*
   11.13    Method.ctxt_args (fn ctxt =>
   11.14 -    Method.METHOD (fn facts => 
   11.15 -      hoare_tac (asm_full_simp_tac (local_simpset_of ctxt))1)) *}
   11.16 +    Method.SIMPLE_METHOD' (hoare_tac (asm_full_simp_tac (local_simpset_of ctxt)))) *}
   11.17    "verification condition generator plus simplification"
   11.18  
   11.19  end
    12.1 --- a/src/HOL/Hoare/HoareAbort.thy	Wed Nov 29 15:44:46 2006 +0100
    12.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Wed Nov 29 15:44:51 2006 +0100
    12.3 @@ -238,14 +238,12 @@
    12.4  use "hoareAbort.ML"
    12.5  
    12.6  method_setup vcg = {*
    12.7 -  Method.no_args
    12.8 -    (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
    12.9 +  Method.no_args (Method.SIMPLE_METHOD' (hoare_tac (K all_tac))) *}
   12.10    "verification condition generator"
   12.11  
   12.12  method_setup vcg_simp = {*
   12.13    Method.ctxt_args (fn ctxt =>
   12.14 -    Method.METHOD (fn facts => 
   12.15 -      hoare_tac (asm_full_simp_tac (local_simpset_of ctxt))1)) *}
   12.16 +    Method.SIMPLE_METHOD' (hoare_tac (asm_full_simp_tac (local_simpset_of ctxt)))) *}
   12.17    "verification condition generator plus simplification"
   12.18  
   12.19  (* Special syntax for guarded statements and guarded array updates: *)
    13.1 --- a/src/HOL/HoareParallel/OG_Tactics.thy	Wed Nov 29 15:44:46 2006 +0100
    13.2 +++ b/src/HOL/HoareParallel/OG_Tactics.thy	Wed Nov 29 15:44:51 2006 +0100
    13.3 @@ -464,25 +464,21 @@
    13.4  Isabelle proofs. *}
    13.5  
    13.6  method_setup oghoare = {*
    13.7 -  Method.no_args
    13.8 -    (Method.SIMPLE_METHOD' HEADGOAL (oghoare_tac)) *}
    13.9 +  Method.no_args (Method.SIMPLE_METHOD' oghoare_tac) *}
   13.10    "verification condition generator for the oghoare logic"
   13.11  
   13.12  method_setup annhoare = {*
   13.13 -  Method.no_args
   13.14 -    (Method.SIMPLE_METHOD' HEADGOAL (annhoare_tac)) *}
   13.15 +  Method.no_args (Method.SIMPLE_METHOD' annhoare_tac) *}
   13.16    "verification condition generator for the ann_hoare logic"
   13.17  
   13.18  method_setup interfree_aux = {*
   13.19 -  Method.no_args
   13.20 -    (Method.SIMPLE_METHOD' HEADGOAL (interfree_aux_tac)) *}
   13.21 +  Method.no_args (Method.SIMPLE_METHOD' interfree_aux_tac) *}
   13.22    "verification condition generator for interference freedom tests"
   13.23  
   13.24  text {* Tactics useful for dealing with the generated verification conditions: *}
   13.25  
   13.26  method_setup conjI_tac = {*
   13.27 -  Method.no_args
   13.28 -    (Method.SIMPLE_METHOD' HEADGOAL (conjI_Tac (K all_tac))) *}
   13.29 +  Method.no_args (Method.SIMPLE_METHOD' (conjI_Tac (K all_tac))) *}
   13.30    "verification condition generator for interference freedom tests"
   13.31  
   13.32  ML {*
   13.33 @@ -493,8 +489,7 @@
   13.34  *}
   13.35  
   13.36  method_setup disjE_tac = {*
   13.37 -  Method.no_args
   13.38 -    (Method.SIMPLE_METHOD' HEADGOAL (disjE_Tac (K all_tac))) *}
   13.39 +  Method.no_args (Method.SIMPLE_METHOD' (disjE_Tac (K all_tac))) *}
   13.40    "verification condition generator for interference freedom tests"
   13.41  
   13.42  end
    14.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Wed Nov 29 15:44:46 2006 +0100
    14.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Wed Nov 29 15:44:51 2006 +0100
    14.3 @@ -183,14 +183,12 @@
    14.4  
    14.5  method_setup fuf = {*
    14.6      Method.ctxt_args (fn ctxt =>
    14.7 -        Method.METHOD (fn facts =>
    14.8 -            fuf_tac (local_clasimpset_of ctxt) 1)) *}
    14.9 +        Method.SIMPLE_METHOD' (fuf_tac (local_clasimpset_of ctxt))) *}
   14.10      "free ultrafilter tactic"
   14.11  
   14.12  method_setup ultra = {*
   14.13      Method.ctxt_args (fn ctxt =>
   14.14 -        Method.METHOD (fn facts =>
   14.15 -            ultra_tac (local_clasimpset_of ctxt) 1)) *}
   14.16 +        Method.SIMPLE_METHOD' (ultra_tac (local_clasimpset_of ctxt))) *}
   14.17      "ultrafilter tactic"
   14.18  
   14.19  
    15.1 --- a/src/HOL/Hyperreal/transfer.ML	Wed Nov 29 15:44:46 2006 +0100
    15.2 +++ b/src/HOL/Hyperreal/transfer.ML	Wed Nov 29 15:44:51 2006 +0100
    15.3 @@ -107,9 +107,6 @@
    15.4    (fn {intros,unfolds,refolds,consts} =>
    15.5      {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
    15.6  
    15.7 -val transfer_method = Method.thms_ctxt_args (fn ths => fn ctxt =>
    15.8 -  Method.SIMPLE_METHOD' HEADGOAL (transfer_tac ctxt ths));
    15.9 -
   15.10  val setup =
   15.11    TransferData.init #>
   15.12    Attrib.add_attributes
   15.13 @@ -119,6 +116,7 @@
   15.14        "declaration of transfer unfolding rule"),
   15.15       ("transfer_refold", Attrib.add_del_args refold_add refold_del,
   15.16        "declaration of transfer refolding rule")] #>
   15.17 -  Method.add_method ("transfer", transfer_method, "transfer principle");
   15.18 +  Method.add_method ("transfer", Method.thms_ctxt_args (fn ths => fn ctxt =>
   15.19 +    Method.SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle");
   15.20  
   15.21  end;
    16.1 --- a/src/HOL/Import/shuffler.ML	Wed Nov 29 15:44:46 2006 +0100
    16.2 +++ b/src/HOL/Import/shuffler.ML	Wed Nov 29 15:44:51 2006 +0100
    16.3 @@ -38,21 +38,21 @@
    16.4  val message = if_debug writeln
    16.5  
    16.6  (*Prints exceptions readably to users*)
    16.7 -fun print_sign_exn_unit sign e = 
    16.8 +fun print_sign_exn_unit sign e =
    16.9    case e of
   16.10       THM (msg,i,thms) =>
   16.11 -	 (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
   16.12 -	  List.app print_thm thms)
   16.13 +         (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
   16.14 +          List.app print_thm thms)
   16.15     | THEORY (msg,thys) =>
   16.16 -	 (writeln ("Exception THEORY raised:\n" ^ msg);
   16.17 -	  List.app (writeln o Context.str_of_thy) thys)
   16.18 +         (writeln ("Exception THEORY raised:\n" ^ msg);
   16.19 +          List.app (writeln o Context.str_of_thy) thys)
   16.20     | TERM (msg,ts) =>
   16.21 -	 (writeln ("Exception TERM raised:\n" ^ msg);
   16.22 -	  List.app (writeln o Sign.string_of_term sign) ts)
   16.23 +         (writeln ("Exception TERM raised:\n" ^ msg);
   16.24 +          List.app (writeln o Sign.string_of_term sign) ts)
   16.25     | TYPE (msg,Ts,ts) =>
   16.26 -	 (writeln ("Exception TYPE raised:\n" ^ msg);
   16.27 -	  List.app (writeln o Sign.string_of_typ sign) Ts;
   16.28 -	  List.app (writeln o Sign.string_of_term sign) ts)
   16.29 +         (writeln ("Exception TYPE raised:\n" ^ msg);
   16.30 +          List.app (writeln o Sign.string_of_typ sign) Ts;
   16.31 +          List.app (writeln o Sign.string_of_term sign) ts)
   16.32     | e => raise e
   16.33  
   16.34  (*Prints an exception, then fails*)
   16.35 @@ -63,14 +63,14 @@
   16.36  
   16.37  fun mk_meta_eq th =
   16.38      (case concl_of th of
   16.39 -	 Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
   16.40 +         Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
   16.41         | Const("==",_) $ _ $ _ => th
   16.42         | _ => raise THM("Not an equality",0,[th]))
   16.43      handle _ => raise THM("Couldn't make meta equality",0,[th])
   16.44 -				   
   16.45 +
   16.46  fun mk_obj_eq th =
   16.47      (case concl_of th of
   16.48 -	 Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th
   16.49 +         Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th
   16.50         | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
   16.51         | _ => raise THM("Not an equality",0,[th]))
   16.52      handle _ => raise THM("Couldn't make object equality",0,[th])
   16.53 @@ -85,113 +85,113 @@
   16.54  fun merge _ = Library.gen_union Thm.eq_thm
   16.55  fun print _ thms =
   16.56      Pretty.writeln (Pretty.big_list "Shuffle theorems:"
   16.57 -				    (map Display.pretty_thm thms))
   16.58 +                                    (map Display.pretty_thm thms))
   16.59  end
   16.60  
   16.61  structure ShuffleData = TheoryDataFun(ShuffleDataArgs)
   16.62  
   16.63  val weaken =
   16.64      let
   16.65 -	val cert = cterm_of ProtoPure.thy
   16.66 -	val P = Free("P",propT)
   16.67 -	val Q = Free("Q",propT)
   16.68 -	val PQ = Logic.mk_implies(P,Q)
   16.69 -	val PPQ = Logic.mk_implies(P,PQ)
   16.70 -	val cP = cert P
   16.71 -	val cQ = cert Q
   16.72 -	val cPQ = cert PQ
   16.73 -	val cPPQ = cert PPQ
   16.74 -	val th1 = assume cPQ |> implies_intr_list [cPQ,cP]
   16.75 -	val th3 = assume cP
   16.76 -	val th4 = implies_elim_list (assume cPPQ) [th3,th3]
   16.77 -				    |> implies_intr_list [cPPQ,cP]
   16.78 +        val cert = cterm_of ProtoPure.thy
   16.79 +        val P = Free("P",propT)
   16.80 +        val Q = Free("Q",propT)
   16.81 +        val PQ = Logic.mk_implies(P,Q)
   16.82 +        val PPQ = Logic.mk_implies(P,PQ)
   16.83 +        val cP = cert P
   16.84 +        val cQ = cert Q
   16.85 +        val cPQ = cert PQ
   16.86 +        val cPPQ = cert PPQ
   16.87 +        val th1 = assume cPQ |> implies_intr_list [cPQ,cP]
   16.88 +        val th3 = assume cP
   16.89 +        val th4 = implies_elim_list (assume cPPQ) [th3,th3]
   16.90 +                                    |> implies_intr_list [cPPQ,cP]
   16.91      in
   16.92 -	equal_intr th4 th1 |> standard
   16.93 +        equal_intr th4 th1 |> standard
   16.94      end
   16.95  
   16.96  val imp_comm =
   16.97      let
   16.98 -	val cert = cterm_of ProtoPure.thy
   16.99 -	val P = Free("P",propT)
  16.100 -	val Q = Free("Q",propT)
  16.101 -	val R = Free("R",propT)
  16.102 -	val PQR = Logic.mk_implies(P,Logic.mk_implies(Q,R))
  16.103 -	val QPR = Logic.mk_implies(Q,Logic.mk_implies(P,R))
  16.104 -	val cP = cert P
  16.105 -	val cQ = cert Q
  16.106 -	val cPQR = cert PQR
  16.107 -	val cQPR = cert QPR
  16.108 -	val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ]
  16.109 -				    |> implies_intr_list [cPQR,cQ,cP]
  16.110 -	val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
  16.111 -				    |> implies_intr_list [cQPR,cP,cQ]
  16.112 +        val cert = cterm_of ProtoPure.thy
  16.113 +        val P = Free("P",propT)
  16.114 +        val Q = Free("Q",propT)
  16.115 +        val R = Free("R",propT)
  16.116 +        val PQR = Logic.mk_implies(P,Logic.mk_implies(Q,R))
  16.117 +        val QPR = Logic.mk_implies(Q,Logic.mk_implies(P,R))
  16.118 +        val cP = cert P
  16.119 +        val cQ = cert Q
  16.120 +        val cPQR = cert PQR
  16.121 +        val cQPR = cert QPR
  16.122 +        val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ]
  16.123 +                                    |> implies_intr_list [cPQR,cQ,cP]
  16.124 +        val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
  16.125 +                                    |> implies_intr_list [cQPR,cP,cQ]
  16.126      in
  16.127 -	equal_intr th1 th2 |> standard
  16.128 +        equal_intr th1 th2 |> standard
  16.129      end
  16.130  
  16.131  val def_norm =
  16.132      let
  16.133 -	val cert = cterm_of ProtoPure.thy
  16.134 -	val aT = TFree("'a",[])
  16.135 -	val bT = TFree("'b",[])
  16.136 -	val v = Free("v",aT)
  16.137 -	val P = Free("P",aT-->bT)
  16.138 -	val Q = Free("Q",aT-->bT)
  16.139 -	val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0)))
  16.140 -	val cPQ = cert (Logic.mk_equals(P,Q))
  16.141 -	val cv = cert v
  16.142 -	val rew = assume cvPQ
  16.143 -			 |> forall_elim cv
  16.144 -			 |> abstract_rule "v" cv
  16.145 -	val (lhs,rhs) = Logic.dest_equals(concl_of rew)
  16.146 -	val th1 = transitive (transitive
  16.147 -				  (eta_conversion (cert lhs) |> symmetric)
  16.148 -				  rew)
  16.149 -			     (eta_conversion (cert rhs))
  16.150 -			     |> implies_intr cvPQ
  16.151 -	val th2 = combination (assume cPQ) (reflexive cv)
  16.152 -			      |> forall_intr cv
  16.153 -			      |> implies_intr cPQ
  16.154 +        val cert = cterm_of ProtoPure.thy
  16.155 +        val aT = TFree("'a",[])
  16.156 +        val bT = TFree("'b",[])
  16.157 +        val v = Free("v",aT)
  16.158 +        val P = Free("P",aT-->bT)
  16.159 +        val Q = Free("Q",aT-->bT)
  16.160 +        val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0)))
  16.161 +        val cPQ = cert (Logic.mk_equals(P,Q))
  16.162 +        val cv = cert v
  16.163 +        val rew = assume cvPQ
  16.164 +                         |> forall_elim cv
  16.165 +                         |> abstract_rule "v" cv
  16.166 +        val (lhs,rhs) = Logic.dest_equals(concl_of rew)
  16.167 +        val th1 = transitive (transitive
  16.168 +                                  (eta_conversion (cert lhs) |> symmetric)
  16.169 +                                  rew)
  16.170 +                             (eta_conversion (cert rhs))
  16.171 +                             |> implies_intr cvPQ
  16.172 +        val th2 = combination (assume cPQ) (reflexive cv)
  16.173 +                              |> forall_intr cv
  16.174 +                              |> implies_intr cPQ
  16.175      in
  16.176 -	equal_intr th1 th2 |> standard
  16.177 +        equal_intr th1 th2 |> standard
  16.178      end
  16.179  
  16.180  val all_comm =
  16.181      let
  16.182 -	val cert = cterm_of ProtoPure.thy
  16.183 -	val xT = TFree("'a",[])
  16.184 -	val yT = TFree("'b",[])
  16.185 -	val P = Free("P",xT-->yT-->propT)
  16.186 -	val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
  16.187 -	val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
  16.188 -	val cl = cert lhs
  16.189 -	val cr = cert rhs
  16.190 -	val cx = cert (Free("x",xT))
  16.191 -	val cy = cert (Free("y",yT))
  16.192 -	val th1 = assume cr
  16.193 -			 |> forall_elim_list [cy,cx]
  16.194 -			 |> forall_intr_list [cx,cy]
  16.195 -			 |> implies_intr cr
  16.196 -	val th2 = assume cl
  16.197 -			 |> forall_elim_list [cx,cy]
  16.198 -			 |> forall_intr_list [cy,cx]
  16.199 -			 |> implies_intr cl
  16.200 +        val cert = cterm_of ProtoPure.thy
  16.201 +        val xT = TFree("'a",[])
  16.202 +        val yT = TFree("'b",[])
  16.203 +        val P = Free("P",xT-->yT-->propT)
  16.204 +        val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
  16.205 +        val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
  16.206 +        val cl = cert lhs
  16.207 +        val cr = cert rhs
  16.208 +        val cx = cert (Free("x",xT))
  16.209 +        val cy = cert (Free("y",yT))
  16.210 +        val th1 = assume cr
  16.211 +                         |> forall_elim_list [cy,cx]
  16.212 +                         |> forall_intr_list [cx,cy]
  16.213 +                         |> implies_intr cr
  16.214 +        val th2 = assume cl
  16.215 +                         |> forall_elim_list [cx,cy]
  16.216 +                         |> forall_intr_list [cy,cx]
  16.217 +                         |> implies_intr cl
  16.218      in
  16.219 -	equal_intr th1 th2 |> standard
  16.220 +        equal_intr th1 th2 |> standard
  16.221      end
  16.222  
  16.223  val equiv_comm =
  16.224      let
  16.225 -	val cert = cterm_of ProtoPure.thy
  16.226 -	val T    = TFree("'a",[])
  16.227 -	val t    = Free("t",T)
  16.228 -	val u    = Free("u",T)
  16.229 -	val ctu  = cert (Logic.mk_equals(t,u))
  16.230 -	val cut  = cert (Logic.mk_equals(u,t))
  16.231 -	val th1  = assume ctu |> symmetric |> implies_intr ctu
  16.232 -	val th2  = assume cut |> symmetric |> implies_intr cut
  16.233 +        val cert = cterm_of ProtoPure.thy
  16.234 +        val T    = TFree("'a",[])
  16.235 +        val t    = Free("t",T)
  16.236 +        val u    = Free("u",T)
  16.237 +        val ctu  = cert (Logic.mk_equals(t,u))
  16.238 +        val cut  = cert (Logic.mk_equals(u,t))
  16.239 +        val th1  = assume ctu |> symmetric |> implies_intr ctu
  16.240 +        val th2  = assume cut |> symmetric |> implies_intr cut
  16.241      in
  16.242 -	equal_intr th1 th2 |> standard
  16.243 +        equal_intr th1 th2 |> standard
  16.244      end
  16.245  
  16.246  (* This simplification procedure rewrites !!x y. P x y
  16.247 @@ -203,82 +203,82 @@
  16.248  exception RESULT of int
  16.249  
  16.250  fun find_bound n (Bound i) = if i = n then raise RESULT 0
  16.251 -			     else if i = n+1 then raise RESULT 1
  16.252 -			     else ()
  16.253 +                             else if i = n+1 then raise RESULT 1
  16.254 +                             else ()
  16.255    | find_bound n (t $ u) = (find_bound n t; find_bound n u)
  16.256    | find_bound n (Abs(_,_,t)) = find_bound (n+1) t
  16.257    | find_bound _ _ = ()
  16.258  
  16.259  fun swap_bound n (Bound i) = if i = n then Bound (n+1)
  16.260 -			     else if i = n+1 then Bound n
  16.261 -			     else Bound i
  16.262 +                             else if i = n+1 then Bound n
  16.263 +                             else Bound i
  16.264    | swap_bound n (t $ u) = (swap_bound n t $ swap_bound n u)
  16.265    | swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t)
  16.266    | swap_bound n t = t
  16.267  
  16.268  fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t =
  16.269      let
  16.270 -	val lhs = list_all ([xv,yv],t)
  16.271 -	val rhs = list_all ([yv,xv],swap_bound 0 t)
  16.272 -	val rew = Logic.mk_equals (lhs,rhs)
  16.273 -	val init = trivial (cterm_of thy rew)
  16.274 +        val lhs = list_all ([xv,yv],t)
  16.275 +        val rhs = list_all ([yv,xv],swap_bound 0 t)
  16.276 +        val rew = Logic.mk_equals (lhs,rhs)
  16.277 +        val init = trivial (cterm_of thy rew)
  16.278      in
  16.279 -	(all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
  16.280 +        (all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
  16.281      end
  16.282  
  16.283  fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
  16.284      let
  16.285 -	val res = (find_bound 0 body;2) handle RESULT i => i
  16.286 +        val res = (find_bound 0 body;2) handle RESULT i => i
  16.287      in
  16.288 -	case res of
  16.289 -	    0 => SOME (rew_th thy (x,xT) (y,yT) body)
  16.290 -	  | 1 => if string_ord(y,x) = LESS
  16.291 -		 then
  16.292 -		     let
  16.293 -			 val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
  16.294 -			 val t_th    = reflexive (cterm_of thy t)
  16.295 -			 val newt_th = reflexive (cterm_of thy newt)
  16.296 -		     in
  16.297 -			 SOME (transitive t_th newt_th)
  16.298 -		     end
  16.299 -		 else NONE
  16.300 -	  | _ => error "norm_term (quant_rewrite) internal error"
  16.301 +        case res of
  16.302 +            0 => SOME (rew_th thy (x,xT) (y,yT) body)
  16.303 +          | 1 => if string_ord(y,x) = LESS
  16.304 +                 then
  16.305 +                     let
  16.306 +                         val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
  16.307 +                         val t_th    = reflexive (cterm_of thy t)
  16.308 +                         val newt_th = reflexive (cterm_of thy newt)
  16.309 +                     in
  16.310 +                         SOME (transitive t_th newt_th)
  16.311 +                     end
  16.312 +                 else NONE
  16.313 +          | _ => error "norm_term (quant_rewrite) internal error"
  16.314       end
  16.315    | quant_rewrite _ _ _ = (warning "quant_rewrite: Unknown lhs"; NONE)
  16.316  
  16.317  fun freeze_thaw_term t =
  16.318      let
  16.319 -	val tvars = term_tvars t
  16.320 -	val tfree_names = add_term_tfree_names(t,[])
  16.321 -	val (type_inst,_) =
  16.322 -	    Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
  16.323 -		      let
  16.324 -			  val v' = Name.variant used v
  16.325 -		      in
  16.326 -			  ((w,TFree(v',S))::inst,v'::used)
  16.327 -		      end)
  16.328 -		  (([],tfree_names),tvars)
  16.329 -	val t' = subst_TVars type_inst t
  16.330 +        val tvars = term_tvars t
  16.331 +        val tfree_names = add_term_tfree_names(t,[])
  16.332 +        val (type_inst,_) =
  16.333 +            Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
  16.334 +                      let
  16.335 +                          val v' = Name.variant used v
  16.336 +                      in
  16.337 +                          ((w,TFree(v',S))::inst,v'::used)
  16.338 +                      end)
  16.339 +                  (([],tfree_names),tvars)
  16.340 +        val t' = subst_TVars type_inst t
  16.341      in
  16.342 -	(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))
  16.343 -		  | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
  16.344 +        (t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))
  16.345 +                  | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
  16.346      end
  16.347  
  16.348  fun inst_tfrees thy [] thm = thm
  16.349 -  | inst_tfrees thy ((name,U)::rest) thm = 
  16.350 +  | inst_tfrees thy ((name,U)::rest) thm =
  16.351      let
  16.352 -	val cU = ctyp_of thy U
  16.353 -	val tfrees = add_term_tfrees (prop_of thm,[])
  16.354 -	val (rens, thm') = Thm.varifyT'
  16.355 +        val cU = ctyp_of thy U
  16.356 +        val tfrees = add_term_tfrees (prop_of thm,[])
  16.357 +        val (rens, thm') = Thm.varifyT'
  16.358      (remove (op = o apsnd fst) name tfrees) thm
  16.359 -	val mid = 
  16.360 -	    case rens of
  16.361 -		[] => thm'
  16.362 -	      | [((_, S), idx)] => instantiate
  16.363 +        val mid =
  16.364 +            case rens of
  16.365 +                [] => thm'
  16.366 +              | [((_, S), idx)] => instantiate
  16.367              ([(ctyp_of thy (TVar (idx, S)), cU)], []) thm'
  16.368 -	      | _ => error "Shuffler.inst_tfrees internal error"
  16.369 +              | _ => error "Shuffler.inst_tfrees internal error"
  16.370      in
  16.371 -	inst_tfrees thy rest mid
  16.372 +        inst_tfrees thy rest mid
  16.373      end
  16.374  
  16.375  fun is_Abs (Abs _) = true
  16.376 @@ -286,65 +286,65 @@
  16.377  
  16.378  fun eta_redex (t $ Bound 0) =
  16.379      let
  16.380 -	fun free n (Bound i) = i = n
  16.381 -	  | free n (t $ u) = free n t orelse free n u
  16.382 -	  | free n (Abs(_,_,t)) = free (n+1) t
  16.383 -	  | free n _ = false
  16.384 +        fun free n (Bound i) = i = n
  16.385 +          | free n (t $ u) = free n t orelse free n u
  16.386 +          | free n (Abs(_,_,t)) = free (n+1) t
  16.387 +          | free n _ = false
  16.388      in
  16.389 -	not (free 0 t)
  16.390 +        not (free 0 t)
  16.391      end
  16.392    | eta_redex _ = false
  16.393  
  16.394  fun eta_contract thy assumes origt =
  16.395      let
  16.396 -	val (typet,Tinst) = freeze_thaw_term origt
  16.397 -	val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
  16.398 -	val final = inst_tfrees thy Tinst o thaw
  16.399 -	val t = #1 (Logic.dest_equals (prop_of init))
  16.400 -	val _ =
  16.401 -	    let
  16.402 -		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
  16.403 -	    in
  16.404 -		if not (lhs aconv origt)
  16.405 -		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
  16.406 -		      writeln (string_of_cterm (cterm_of thy origt));
  16.407 -		      writeln (string_of_cterm (cterm_of thy lhs));
  16.408 -		      writeln (string_of_cterm (cterm_of thy typet));
  16.409 -		      writeln (string_of_cterm (cterm_of thy t));
  16.410 -		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
  16.411 -		      writeln "done")
  16.412 -		else ()
  16.413 -	    end
  16.414 +        val (typet,Tinst) = freeze_thaw_term origt
  16.415 +        val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
  16.416 +        val final = inst_tfrees thy Tinst o thaw
  16.417 +        val t = #1 (Logic.dest_equals (prop_of init))
  16.418 +        val _ =
  16.419 +            let
  16.420 +                val lhs = #1 (Logic.dest_equals (prop_of (final init)))
  16.421 +            in
  16.422 +                if not (lhs aconv origt)
  16.423 +                then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
  16.424 +                      writeln (string_of_cterm (cterm_of thy origt));
  16.425 +                      writeln (string_of_cterm (cterm_of thy lhs));
  16.426 +                      writeln (string_of_cterm (cterm_of thy typet));
  16.427 +                      writeln (string_of_cterm (cterm_of thy t));
  16.428 +                      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
  16.429 +                      writeln "done")
  16.430 +                else ()
  16.431 +            end
  16.432      in
  16.433 -	case t of
  16.434 -	    Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) =>
  16.435 -	    ((if eta_redex P andalso eta_redex Q
  16.436 -	      then
  16.437 -		  let
  16.438 -		      val cert = cterm_of thy
  16.439 -		      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
  16.440 -		      val cv = cert v
  16.441 -		      val ct = cert t
  16.442 -		      val th = (assume ct)
  16.443 -				   |> forall_elim cv
  16.444 -				   |> abstract_rule x cv
  16.445 -		      val ext_th = eta_conversion (cert (Abs(x,xT,P)))
  16.446 -		      val th' = transitive (symmetric ext_th) th
  16.447 -		      val cu = cert (prop_of th')
  16.448 -		      val uth = combination (assume cu) (reflexive cv)
  16.449 -		      val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v)))
  16.450 -				     |> transitive uth
  16.451 -				     |> forall_intr cv
  16.452 -				     |> implies_intr cu
  16.453 -		      val rew_th = equal_intr (th' |> implies_intr ct) uth'
  16.454 -		      val res = final rew_th
  16.455 -		      val lhs = (#1 (Logic.dest_equals (prop_of res)))
  16.456 -		  in
  16.457 -		       SOME res
  16.458 -		  end
  16.459 -	      else NONE)
  16.460 -	     handle e => OldGoals.print_exn e)
  16.461 -	  | _ => NONE
  16.462 +        case t of
  16.463 +            Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) =>
  16.464 +            ((if eta_redex P andalso eta_redex Q
  16.465 +              then
  16.466 +                  let
  16.467 +                      val cert = cterm_of thy
  16.468 +                      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
  16.469 +                      val cv = cert v
  16.470 +                      val ct = cert t
  16.471 +                      val th = (assume ct)
  16.472 +                                   |> forall_elim cv
  16.473 +                                   |> abstract_rule x cv
  16.474 +                      val ext_th = eta_conversion (cert (Abs(x,xT,P)))
  16.475 +                      val th' = transitive (symmetric ext_th) th
  16.476 +                      val cu = cert (prop_of th')
  16.477 +                      val uth = combination (assume cu) (reflexive cv)
  16.478 +                      val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v)))
  16.479 +                                     |> transitive uth
  16.480 +                                     |> forall_intr cv
  16.481 +                                     |> implies_intr cu
  16.482 +                      val rew_th = equal_intr (th' |> implies_intr ct) uth'
  16.483 +                      val res = final rew_th
  16.484 +                      val lhs = (#1 (Logic.dest_equals (prop_of res)))
  16.485 +                  in
  16.486 +                       SOME res
  16.487 +                  end
  16.488 +              else NONE)
  16.489 +             handle e => OldGoals.print_exn e)
  16.490 +          | _ => NONE
  16.491         end
  16.492  
  16.493  fun beta_fun thy assume t =
  16.494 @@ -354,62 +354,62 @@
  16.495  
  16.496  fun equals_fun thy assume t =
  16.497      case t of
  16.498 -	Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
  16.499 +        Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
  16.500        | _ => NONE
  16.501  
  16.502  fun eta_expand thy assumes origt =
  16.503      let
  16.504 -	val (typet,Tinst) = freeze_thaw_term origt
  16.505 -	val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
  16.506 -	val final = inst_tfrees thy Tinst o thaw
  16.507 -	val t = #1 (Logic.dest_equals (prop_of init))
  16.508 -	val _ =
  16.509 -	    let
  16.510 -		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
  16.511 -	    in
  16.512 -		if not (lhs aconv origt)
  16.513 -		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
  16.514 -		      writeln (string_of_cterm (cterm_of thy origt));
  16.515 -		      writeln (string_of_cterm (cterm_of thy lhs));
  16.516 -		      writeln (string_of_cterm (cterm_of thy typet));
  16.517 -		      writeln (string_of_cterm (cterm_of thy t));
  16.518 -		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
  16.519 -		      writeln "done")
  16.520 -		else ()
  16.521 -	    end
  16.522 +        val (typet,Tinst) = freeze_thaw_term origt
  16.523 +        val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
  16.524 +        val final = inst_tfrees thy Tinst o thaw
  16.525 +        val t = #1 (Logic.dest_equals (prop_of init))
  16.526 +        val _ =
  16.527 +            let
  16.528 +                val lhs = #1 (Logic.dest_equals (prop_of (final init)))
  16.529 +            in
  16.530 +                if not (lhs aconv origt)
  16.531 +                then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
  16.532 +                      writeln (string_of_cterm (cterm_of thy origt));
  16.533 +                      writeln (string_of_cterm (cterm_of thy lhs));
  16.534 +                      writeln (string_of_cterm (cterm_of thy typet));
  16.535 +                      writeln (string_of_cterm (cterm_of thy t));
  16.536 +                      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
  16.537 +                      writeln "done")
  16.538 +                else ()
  16.539 +            end
  16.540      in
  16.541 -	case t of
  16.542 -	    Const("==",T) $ P $ Q =>
  16.543 -	    if is_Abs P orelse is_Abs Q
  16.544 -	    then (case domain_type T of
  16.545 -		      Type("fun",[aT,bT]) =>
  16.546 -		      let
  16.547 -			  val cert = cterm_of thy
  16.548 -			  val vname = Name.variant (add_term_free_names(t,[])) "v"
  16.549 -			  val v = Free(vname,aT)
  16.550 -			  val cv = cert v
  16.551 -			  val ct = cert t
  16.552 -			  val th1 = (combination (assume ct) (reflexive cv))
  16.553 -					|> forall_intr cv
  16.554 -					|> implies_intr ct
  16.555 -			  val concl = cert (concl_of th1)
  16.556 -			  val th2 = (assume concl)
  16.557 -					|> forall_elim cv
  16.558 -					|> abstract_rule vname cv
  16.559 -			  val (lhs,rhs) = Logic.dest_equals (prop_of th2)
  16.560 -			  val elhs = eta_conversion (cert lhs)
  16.561 -			  val erhs = eta_conversion (cert rhs)
  16.562 -			  val th2' = transitive
  16.563 -					 (transitive (symmetric elhs) th2)
  16.564 -					 erhs
  16.565 -			  val res = equal_intr th1 (th2' |> implies_intr concl)
  16.566 -			  val res' = final res
  16.567 -		      in
  16.568 -			  SOME res'
  16.569 -		      end
  16.570 -		    | _ => NONE)
  16.571 -	    else NONE
  16.572 -	  | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
  16.573 +        case t of
  16.574 +            Const("==",T) $ P $ Q =>
  16.575 +            if is_Abs P orelse is_Abs Q
  16.576 +            then (case domain_type T of
  16.577 +                      Type("fun",[aT,bT]) =>
  16.578 +                      let
  16.579 +                          val cert = cterm_of thy
  16.580 +                          val vname = Name.variant (add_term_free_names(t,[])) "v"
  16.581 +                          val v = Free(vname,aT)
  16.582 +                          val cv = cert v
  16.583 +                          val ct = cert t
  16.584 +                          val th1 = (combination (assume ct) (reflexive cv))
  16.585 +                                        |> forall_intr cv
  16.586 +                                        |> implies_intr ct
  16.587 +                          val concl = cert (concl_of th1)
  16.588 +                          val th2 = (assume concl)
  16.589 +                                        |> forall_elim cv
  16.590 +                                        |> abstract_rule vname cv
  16.591 +                          val (lhs,rhs) = Logic.dest_equals (prop_of th2)
  16.592 +                          val elhs = eta_conversion (cert lhs)
  16.593 +                          val erhs = eta_conversion (cert rhs)
  16.594 +                          val th2' = transitive
  16.595 +                                         (transitive (symmetric elhs) th2)
  16.596 +                                         erhs
  16.597 +                          val res = equal_intr th1 (th2' |> implies_intr concl)
  16.598 +                          val res' = final res
  16.599 +                      in
  16.600 +                          SOME res'
  16.601 +                      end
  16.602 +                    | _ => NONE)
  16.603 +            else NONE
  16.604 +          | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
  16.605      end
  16.606      handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
  16.607  
  16.608 @@ -424,32 +424,32 @@
  16.609  val S'  = mk_free "S'" xT
  16.610  in
  16.611  fun beta_simproc thy = Simplifier.simproc_i
  16.612 -		      thy
  16.613 -		      "Beta-contraction"
  16.614 -		      [Abs("x",xT,Q) $ S]
  16.615 -		      beta_fun
  16.616 +                      thy
  16.617 +                      "Beta-contraction"
  16.618 +                      [Abs("x",xT,Q) $ S]
  16.619 +                      beta_fun
  16.620  
  16.621  fun equals_simproc thy = Simplifier.simproc_i
  16.622 -		      thy
  16.623 -		      "Ordered rewriting of meta equalities"
  16.624 -		      [Const("op ==",xT) $ S $ S']
  16.625 -		      equals_fun
  16.626 +                      thy
  16.627 +                      "Ordered rewriting of meta equalities"
  16.628 +                      [Const("op ==",xT) $ S $ S']
  16.629 +                      equals_fun
  16.630  
  16.631  fun quant_simproc thy = Simplifier.simproc_i
  16.632 -			   thy
  16.633 -			   "Ordered rewriting of nested quantifiers"
  16.634 -			   [all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
  16.635 -			   quant_rewrite
  16.636 +                           thy
  16.637 +                           "Ordered rewriting of nested quantifiers"
  16.638 +                           [all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
  16.639 +                           quant_rewrite
  16.640  fun eta_expand_simproc thy = Simplifier.simproc_i
  16.641 -			 thy
  16.642 -			 "Smart eta-expansion by equivalences"
  16.643 -			 [Logic.mk_equals(Q,R)]
  16.644 -			 eta_expand
  16.645 +                         thy
  16.646 +                         "Smart eta-expansion by equivalences"
  16.647 +                         [Logic.mk_equals(Q,R)]
  16.648 +                         eta_expand
  16.649  fun eta_contract_simproc thy = Simplifier.simproc_i
  16.650 -			 thy
  16.651 -			 "Smart handling of eta-contractions"
  16.652 -			 [all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
  16.653 -			 eta_contract
  16.654 +                         thy
  16.655 +                         "Smart handling of eta-contractions"
  16.656 +                         [all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
  16.657 +                         eta_contract
  16.658  end
  16.659  
  16.660  (* Disambiguates the names of bound variables in a term, returning t
  16.661 @@ -457,29 +457,29 @@
  16.662  
  16.663  fun disamb_bound thy t =
  16.664      let
  16.665 -	
  16.666 -	fun F (t $ u,idx) =
  16.667 -	    let
  16.668 -		val (t',idx') = F (t,idx)
  16.669 -		val (u',idx'') = F (u,idx')
  16.670 -	    in
  16.671 -		(t' $ u',idx'')
  16.672 -	    end
  16.673 -	  | F (Abs(x,xT,t),idx) =
  16.674 -	    let
  16.675 -		val x' = "x" ^ (LargeInt.toString idx) (* amazing *)
  16.676 -		val (t',idx') = F (t,idx+1)
  16.677 -	    in
  16.678 -		(Abs(x',xT,t'),idx')
  16.679 -	    end
  16.680 -	  | F arg = arg
  16.681 -	val (t',_) = F (t,0)
  16.682 -	val ct = cterm_of thy t
  16.683 -	val ct' = cterm_of thy t'
  16.684 -	val res = transitive (reflexive ct) (reflexive ct')
  16.685 -	val _ = message ("disamb_term: " ^ (string_of_thm res))
  16.686 +
  16.687 +        fun F (t $ u,idx) =
  16.688 +            let
  16.689 +                val (t',idx') = F (t,idx)
  16.690 +                val (u',idx'') = F (u,idx')
  16.691 +            in
  16.692 +                (t' $ u',idx'')
  16.693 +            end
  16.694 +          | F (Abs(x,xT,t),idx) =
  16.695 +            let
  16.696 +                val x' = "x" ^ (LargeInt.toString idx) (* amazing *)
  16.697 +                val (t',idx') = F (t,idx+1)
  16.698 +            in
  16.699 +                (Abs(x',xT,t'),idx')
  16.700 +            end
  16.701 +          | F arg = arg
  16.702 +        val (t',_) = F (t,0)
  16.703 +        val ct = cterm_of thy t
  16.704 +        val ct' = cterm_of thy t'
  16.705 +        val res = transitive (reflexive ct) (reflexive ct')
  16.706 +        val _ = message ("disamb_term: " ^ (string_of_thm res))
  16.707      in
  16.708 -	res
  16.709 +        res
  16.710      end
  16.711  
  16.712  (* Transforms a term t to some normal form t', returning the theorem t
  16.713 @@ -488,25 +488,25 @@
  16.714  
  16.715  fun norm_term thy t =
  16.716      let
  16.717 -	val norms = ShuffleData.get thy
  16.718 -	val ss = Simplifier.theory_context thy empty_ss
  16.719 +        val norms = ShuffleData.get thy
  16.720 +        val ss = Simplifier.theory_context thy empty_ss
  16.721            setmksimps single
  16.722 -	  addsimps (map (Thm.transfer thy) norms)
  16.723 +          addsimps (map (Thm.transfer thy) norms)
  16.724            addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
  16.725 -	fun chain f th =
  16.726 -	    let
  16.727 +        fun chain f th =
  16.728 +            let
  16.729                  val rhs = snd (dest_equals (cprop_of th))
  16.730 -      	    in
  16.731 -		transitive th (f rhs)
  16.732 -	    end
  16.733 -	val th =
  16.734 +            in
  16.735 +                transitive th (f rhs)
  16.736 +            end
  16.737 +        val th =
  16.738              t |> disamb_bound thy
  16.739 -	      |> chain (Simplifier.full_rewrite ss)
  16.740 +              |> chain (Simplifier.full_rewrite ss)
  16.741                |> chain eta_conversion
  16.742 -	      |> strip_shyps
  16.743 -	val _ = message ("norm_term: " ^ (string_of_thm th))
  16.744 +              |> strip_shyps
  16.745 +        val _ = message ("norm_term: " ^ (string_of_thm th))
  16.746      in
  16.747 -	th
  16.748 +        th
  16.749      end
  16.750      handle e => (writeln "norm_term internal error"; print_sign_exn thy e)
  16.751  
  16.752 @@ -516,11 +516,11 @@
  16.753  
  16.754  fun close_thm th =
  16.755      let
  16.756 -	val thy = sign_of_thm th
  16.757 -	val c = prop_of th
  16.758 -	val vars = add_term_frees (c,add_term_vars(c,[]))
  16.759 +        val thy = sign_of_thm th
  16.760 +        val c = prop_of th
  16.761 +        val vars = add_term_frees (c,add_term_vars(c,[]))
  16.762      in
  16.763 -	Drule.forall_intr_list (map (cterm_of thy) vars) th
  16.764 +        Drule.forall_intr_list (map (cterm_of thy) vars) th
  16.765      end
  16.766      handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
  16.767  
  16.768 @@ -528,9 +528,9 @@
  16.769  
  16.770  fun norm_thm thy th =
  16.771      let
  16.772 -	val c = prop_of th
  16.773 +        val c = prop_of th
  16.774      in
  16.775 -	equal_elim (norm_term thy c) th
  16.776 +        equal_elim (norm_term thy c) th
  16.777      end
  16.778  
  16.779  (* make_equal thy t u tries to construct the theorem t == u under the
  16.780 @@ -539,43 +539,43 @@
  16.781  
  16.782  fun make_equal thy t u =
  16.783      let
  16.784 -	val t_is_t' = norm_term thy t
  16.785 -	val u_is_u' = norm_term thy u
  16.786 -	val th = transitive t_is_t' (symmetric u_is_u')
  16.787 -	val _ = message ("make_equal: SOME " ^ (string_of_thm th))
  16.788 +        val t_is_t' = norm_term thy t
  16.789 +        val u_is_u' = norm_term thy u
  16.790 +        val th = transitive t_is_t' (symmetric u_is_u')
  16.791 +        val _ = message ("make_equal: SOME " ^ (string_of_thm th))
  16.792      in
  16.793 -	SOME th
  16.794 +        SOME th
  16.795      end
  16.796      handle e as THM _ => (message "make_equal: NONE";NONE)
  16.797 -			 
  16.798 +
  16.799  fun match_consts ignore t (* th *) =
  16.800      let
  16.801 -	fun add_consts (Const (c, _), cs) =
  16.802 -	    if c mem_string ignore
  16.803 -	    then cs
  16.804 -	    else insert (op =) c cs
  16.805 -	  | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
  16.806 -	  | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
  16.807 -	  | add_consts (_, cs) = cs
  16.808 -	val t_consts = add_consts(t,[])
  16.809 +        fun add_consts (Const (c, _), cs) =
  16.810 +            if c mem_string ignore
  16.811 +            then cs
  16.812 +            else insert (op =) c cs
  16.813 +          | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
  16.814 +          | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
  16.815 +          | add_consts (_, cs) = cs
  16.816 +        val t_consts = add_consts(t,[])
  16.817      in
  16.818       fn (name,th) =>
  16.819 -	let
  16.820 -	    val th_consts = add_consts(prop_of th,[])
  16.821 -	in
  16.822 -	    eq_set(t_consts,th_consts)
  16.823 -	end
  16.824 +        let
  16.825 +            val th_consts = add_consts(prop_of th,[])
  16.826 +        in
  16.827 +            eq_set(t_consts,th_consts)
  16.828 +        end
  16.829      end
  16.830 -    
  16.831 +
  16.832  val collect_ignored =
  16.833      fold_rev (fn thm => fn cs =>
  16.834 -	      let
  16.835 -		  val (lhs,rhs) = Logic.dest_equals (prop_of thm)
  16.836 -		  val ignore_lhs = term_consts lhs \\ term_consts rhs
  16.837 -		  val ignore_rhs = term_consts rhs \\ term_consts lhs
  16.838 -	      in
  16.839 -		  fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
  16.840 -	      end)
  16.841 +              let
  16.842 +                  val (lhs,rhs) = Logic.dest_equals (prop_of thm)
  16.843 +                  val ignore_lhs = term_consts lhs \\ term_consts rhs
  16.844 +                  val ignore_rhs = term_consts rhs \\ term_consts lhs
  16.845 +              in
  16.846 +                  fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
  16.847 +              end)
  16.848  
  16.849  (* set_prop t thms tries to make a theorem with the proposition t from
  16.850  one of the theorems thms, by shuffling the propositions around.  If it
  16.851 @@ -583,67 +583,67 @@
  16.852  
  16.853  fun set_prop thy t =
  16.854      let
  16.855 -	val vars = add_term_frees (t,add_term_vars (t,[]))
  16.856 -	val closed_t = Library.foldr (fn (v, body) =>
  16.857 +        val vars = add_term_frees (t,add_term_vars (t,[]))
  16.858 +        val closed_t = Library.foldr (fn (v, body) =>
  16.859        let val vT = type_of v in all vT $ (Abs ("x", vT, abstract_over (v, body))) end) (vars, t)
  16.860 -	val rew_th = norm_term thy closed_t
  16.861 -	val rhs = snd (dest_equals (cprop_of rew_th))
  16.862 +        val rew_th = norm_term thy closed_t
  16.863 +        val rhs = snd (dest_equals (cprop_of rew_th))
  16.864  
  16.865 -	val shuffles = ShuffleData.get thy
  16.866 -	fun process [] = NONE
  16.867 -	  | process ((name,th)::thms) =
  16.868 -	    let
  16.869 -		val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
  16.870 -		val triv_th = trivial rhs
  16.871 -		val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
  16.872 -		val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
  16.873 -				 SOME(th,_) => SOME th
  16.874 -			       | NONE => NONE
  16.875 -	    in
  16.876 -		case mod_th of
  16.877 -		    SOME mod_th =>
  16.878 -		    let
  16.879 -			val closed_th = equal_elim (symmetric rew_th) mod_th
  16.880 -		    in
  16.881 -			message ("Shuffler.set_prop succeeded by " ^ name);
  16.882 -			SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
  16.883 -		    end
  16.884 -		  | NONE => process thms
  16.885 -	    end
  16.886 -	    handle e as THM _ => process thms
  16.887 +        val shuffles = ShuffleData.get thy
  16.888 +        fun process [] = NONE
  16.889 +          | process ((name,th)::thms) =
  16.890 +            let
  16.891 +                val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
  16.892 +                val triv_th = trivial rhs
  16.893 +                val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
  16.894 +                val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
  16.895 +                                 SOME(th,_) => SOME th
  16.896 +                               | NONE => NONE
  16.897 +            in
  16.898 +                case mod_th of
  16.899 +                    SOME mod_th =>
  16.900 +                    let
  16.901 +                        val closed_th = equal_elim (symmetric rew_th) mod_th
  16.902 +                    in
  16.903 +                        message ("Shuffler.set_prop succeeded by " ^ name);
  16.904 +                        SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
  16.905 +                    end
  16.906 +                  | NONE => process thms
  16.907 +            end
  16.908 +            handle e as THM _ => process thms
  16.909      in
  16.910 -	fn thms =>
  16.911 -	   case process thms of
  16.912 -	       res as SOME (name,th) => if (prop_of th) aconv t
  16.913 -					then res
  16.914 -					else error "Internal error in set_prop"
  16.915 -	     | NONE => NONE
  16.916 +        fn thms =>
  16.917 +           case process thms of
  16.918 +               res as SOME (name,th) => if (prop_of th) aconv t
  16.919 +                                        then res
  16.920 +                                        else error "Internal error in set_prop"
  16.921 +             | NONE => NONE
  16.922      end
  16.923      handle e => (writeln "set_prop internal error"; OldGoals.print_exn e)
  16.924  
  16.925  fun find_potential thy t =
  16.926      let
  16.927 -	val shuffles = ShuffleData.get thy
  16.928 -	val ignored = collect_ignored shuffles []
  16.929 -	val rel_consts = term_consts t \\ ignored
  16.930 -	val pot_thms = PureThy.thms_containing_consts thy rel_consts
  16.931 +        val shuffles = ShuffleData.get thy
  16.932 +        val ignored = collect_ignored shuffles []
  16.933 +        val rel_consts = term_consts t \\ ignored
  16.934 +        val pot_thms = PureThy.thms_containing_consts thy rel_consts
  16.935      in
  16.936 -	List.filter (match_consts ignored t) pot_thms
  16.937 +        List.filter (match_consts ignored t) pot_thms
  16.938      end
  16.939  
  16.940  fun gen_shuffle_tac thy search thms i st =
  16.941      let
  16.942 -	val _ = message ("Shuffling " ^ (string_of_thm st))
  16.943 -	val t = List.nth(prems_of st,i-1)
  16.944 -	val set = set_prop thy t
  16.945 -	fun process_tac thms st =
  16.946 -	    case set thms of
  16.947 -		SOME (_,th) => Seq.of_list (compose (th,i,st))
  16.948 -	      | NONE => Seq.empty
  16.949 +        val _ = message ("Shuffling " ^ (string_of_thm st))
  16.950 +        val t = List.nth(prems_of st,i-1)
  16.951 +        val set = set_prop thy t
  16.952 +        fun process_tac thms st =
  16.953 +            case set thms of
  16.954 +                SOME (_,th) => Seq.of_list (compose (th,i,st))
  16.955 +              | NONE => Seq.empty
  16.956      in
  16.957 -	(process_tac thms APPEND (if search
  16.958 -				  then process_tac (find_potential thy t)
  16.959 -				  else no_tac)) st
  16.960 +        (process_tac thms APPEND (if search
  16.961 +                                  then process_tac (find_potential thy t)
  16.962 +                                  else no_tac)) st
  16.963      end
  16.964  
  16.965  fun shuffle_tac thms i st =
  16.966 @@ -654,29 +654,29 @@
  16.967  
  16.968  fun shuffle_meth (thms:thm list) ctxt =
  16.969      let
  16.970 -	val thy = ProofContext.theory_of ctxt
  16.971 +        val thy = ProofContext.theory_of ctxt
  16.972      in
  16.973 -	Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy false (map (pair "") thms))
  16.974 +        Method.SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms))
  16.975      end
  16.976  
  16.977  fun search_meth ctxt =
  16.978      let
  16.979 -	val thy = ProofContext.theory_of ctxt
  16.980 -	val prems = Assumption.prems_of ctxt
  16.981 +        val thy = ProofContext.theory_of ctxt
  16.982 +        val prems = Assumption.prems_of ctxt
  16.983      in
  16.984 -	Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy true (map (pair "premise") prems))
  16.985 +        Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
  16.986      end
  16.987  
  16.988  val print_shuffles = ShuffleData.print
  16.989  
  16.990  fun add_shuffle_rule thm thy =
  16.991      let
  16.992 -	val shuffles = ShuffleData.get thy
  16.993 +        val shuffles = ShuffleData.get thy
  16.994      in
  16.995 -	if exists (curry Thm.eq_thm thm) shuffles
  16.996 -	then (warning ((string_of_thm thm) ^ " already known to the shuffler");
  16.997 -	      thy)
  16.998 -	else ShuffleData.put (thm::shuffles) thy
  16.999 +        if exists (curry Thm.eq_thm thm) shuffles
 16.1000 +        then (warning ((string_of_thm thm) ^ " already known to the shuffler");
 16.1001 +              thy)
 16.1002 +        else ShuffleData.put (thm::shuffles) thy
 16.1003      end
 16.1004  
 16.1005  val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
    17.1 --- a/src/HOL/Integ/presburger.ML	Wed Nov 29 15:44:46 2006 +0100
    17.2 +++ b/src/HOL/Integ/presburger.ML	Wed Nov 29 15:44:51 2006 +0100
    17.3 @@ -10,10 +10,9 @@
    17.4  call the procedure with the parameter abs.
    17.5  *)
    17.6  
    17.7 -signature PRESBURGER = 
    17.8 +signature PRESBURGER =
    17.9  sig
   17.10   val presburger_tac : bool -> bool -> int -> tactic
   17.11 - val presburger_method : bool -> bool -> int -> Proof.method
   17.12   val setup : theory -> theory
   17.13   val trace : bool ref
   17.14  end;
   17.15 @@ -25,7 +24,7 @@
   17.16  fun trace_msg s = if !trace then tracing s else ();
   17.17  
   17.18  (*-----------------------------------------------------------------*)
   17.19 -(*cooper_pp: provefunction for the one-exstance quantifier elimination*)
   17.20 +(*cooper_pp: provefunction for the one-existance quantifier elimination*)
   17.21  (* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
   17.22  (*-----------------------------------------------------------------*)
   17.23  
   17.24 @@ -36,35 +35,35 @@
   17.25   "pred_Pls","pred_Min","pred_1","pred_0",
   17.26    "succ_Pls", "succ_Min", "succ_1", "succ_0",
   17.27    "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
   17.28 -  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1", 
   17.29 -  "minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0", 
   17.30 +  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1",
   17.31 +  "minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0",
   17.32    "add_Pls_right", "add_Min_right"];
   17.33 - val intarithrel = 
   17.34 -     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
   17.35 -		"int_le_number_of_eq","int_iszero_number_of_0",
   17.36 -		"int_less_number_of_eq_neg"]) @
   17.37 -     (map (fn s => thm s RS thm "lift_bool") 
   17.38 -	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
   17.39 -	   "int_neg_number_of_Min"])@
   17.40 -     (map (fn s => thm s RS thm "nlift_bool") 
   17.41 -	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
   17.42 -     
   17.43 + val intarithrel =
   17.44 +     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT",
   17.45 +                "int_le_number_of_eq","int_iszero_number_of_0",
   17.46 +                "int_less_number_of_eq_neg"]) @
   17.47 +     (map (fn s => thm s RS thm "lift_bool")
   17.48 +          ["int_iszero_number_of_Pls","int_iszero_number_of_1",
   17.49 +           "int_neg_number_of_Min"])@
   17.50 +     (map (fn s => thm s RS thm "nlift_bool")
   17.51 +          ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
   17.52 +
   17.53  val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
   17.54 -			"int_number_of_diff_sym", "int_number_of_mult_sym"];
   17.55 +                        "int_number_of_diff_sym", "int_number_of_mult_sym"];
   17.56  val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
   17.57 -			"mult_nat_number_of", "eq_nat_number_of",
   17.58 -			"less_nat_number_of"]
   17.59 -val powerarith = 
   17.60 -    (map thm ["nat_number_of", "zpower_number_of_even", 
   17.61 -	      "zpower_Pls", "zpower_Min"]) @ 
   17.62 -    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
   17.63 -			   thm "one_eq_Numeral1_nring"] 
   17.64 +                        "mult_nat_number_of", "eq_nat_number_of",
   17.65 +                        "less_nat_number_of"]
   17.66 +val powerarith =
   17.67 +    (map thm ["nat_number_of", "zpower_number_of_even",
   17.68 +              "zpower_Pls", "zpower_Min"]) @
   17.69 +    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring",
   17.70 +                           thm "one_eq_Numeral1_nring"]
   17.71    (thm "zpower_number_of_odd"))]
   17.72  
   17.73 -val comp_arith = binarith @ intarith @ intarithrel @ natarith 
   17.74 -	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
   17.75 +val comp_arith = binarith @ intarith @ intarithrel @ natarith
   17.76 +            @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
   17.77  
   17.78 -fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
   17.79 +fun cooper_pp sg (fm as e$Abs(xn,xT,p)) =
   17.80    let val (xn1,p1) = Syntax.variant_abs (xn,xT,p)
   17.81    in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
   17.82  
   17.83 @@ -140,7 +139,7 @@
   17.84     ("Divides.mod", iT --> iT --> iT),
   17.85     ("HOL.plus", iT --> iT --> iT),
   17.86     ("HOL.minus", iT --> iT --> iT),
   17.87 -   ("HOL.times", iT --> iT --> iT), 
   17.88 +   ("HOL.times", iT --> iT --> iT),
   17.89     ("HOL.abs", iT --> iT),
   17.90     ("HOL.uminus", iT --> iT),
   17.91     ("HOL.max", iT --> iT --> iT),
   17.92 @@ -154,7 +153,7 @@
   17.93     ("Divides.mod", nT --> nT --> nT),
   17.94     ("HOL.plus", nT --> nT --> nT),
   17.95     ("HOL.minus", nT --> nT --> nT),
   17.96 -   ("HOL.times", nT --> nT --> nT), 
   17.97 +   ("HOL.times", nT --> nT --> nT),
   17.98     ("Suc", nT --> nT),
   17.99     ("HOL.max", nT --> nT --> nT),
  17.100     ("HOL.min", nT --> nT --> nT),
  17.101 @@ -186,12 +185,12 @@
  17.102  
  17.103  fun getfuncs fm = case strip_comb fm of
  17.104      (Free (_, T), ts as _ :: _) =>
  17.105 -      if body_type T mem [iT, nT] 
  17.106 -         andalso not (ts = []) andalso forall (null o loose_bnos) ts 
  17.107 +      if body_type T mem [iT, nT]
  17.108 +         andalso not (ts = []) andalso forall (null o loose_bnos) ts
  17.109        then [fm]
  17.110        else Library.foldl op union ([], map getfuncs ts)
  17.111    | (Var (_, T), ts as _ :: _) =>
  17.112 -      if body_type T mem [iT, nT] 
  17.113 +      if body_type T mem [iT, nT]
  17.114           andalso not (ts = []) andalso forall (null o loose_bnos) ts then [fm]
  17.115        else Library.foldl op union ([], map getfuncs ts)
  17.116    | (Const (s, T), ts) =>
  17.117 @@ -202,7 +201,7 @@
  17.118    | _ => [];
  17.119  
  17.120  
  17.121 -fun abstract_pres sg fm = 
  17.122 +fun abstract_pres sg fm =
  17.123    foldr (fn (t, u) =>
  17.124        let val T = fastype_of t
  17.125        in all T $ Abs ("x", T, abstract_over (t, u)) end)
  17.126 @@ -214,11 +213,11 @@
  17.127   It returns true if there is a subterm coresponding to the application of
  17.128   a function on a bounded variable.
  17.129  
  17.130 - Function applications are allowed only for well predefined functions a 
  17.131 + Function applications are allowed only for well predefined functions a
  17.132   consts*)
  17.133  
  17.134  fun has_free_funcs fm  = case strip_comb fm of
  17.135 -    (Free (_, T), ts as _ :: _) => 
  17.136 +    (Free (_, T), ts as _ :: _) =>
  17.137        if (body_type T mem [iT,nT]) andalso (not (T mem [iT,nT]))
  17.138        then true
  17.139        else exists (fn x => x) (map has_free_funcs ts)
  17.140 @@ -233,24 +232,24 @@
  17.141  
  17.142  (*returns true if the formula is relevant for presburger arithmetic tactic
  17.143  The constants occuring in term t should be a subset of the allowed_consts
  17.144 - There also should be no occurences of application of functions on bounded 
  17.145 - variables. Whenever this function will be used, it will be ensured that t 
  17.146 - will not contain subterms with function symbols that could have been 
  17.147 + There also should be no occurences of application of functions on bounded
  17.148 + variables. Whenever this function will be used, it will be ensured that t
  17.149 + will not contain subterms with function symbols that could have been
  17.150   abstracted over.*)
  17.151 - 
  17.152 -fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso 
  17.153 +
  17.154 +fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso
  17.155    map (fn i => snd (List.nth (ps, i))) (loose_bnos t) @
  17.156    map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
  17.157    subset [iT, nT]
  17.158    andalso not (has_free_funcs t);
  17.159  
  17.160  
  17.161 -fun prepare_for_presburger sg q fm = 
  17.162 +fun prepare_for_presburger sg q fm =
  17.163    let
  17.164      val ps = Logic.strip_params fm
  17.165      val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
  17.166      val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
  17.167 -    val _ = if relevant (rev ps) c then () 
  17.168 +    val _ = if relevant (rev ps) c then ()
  17.169                 else  (trace_msg ("Conclusion is not a presburger term:\n" ^
  17.170               Sign.string_of_term sg c); raise CooperDec.COOPER)
  17.171      fun mk_all ((s, T), (P,n)) =
  17.172 @@ -275,7 +274,7 @@
  17.173  
  17.174  (* the presburger tactic*)
  17.175  
  17.176 -(* Parameters : q = flag for quantify ofer free variables ; 
  17.177 +(* Parameters : q = flag for quantify ofer free variables ;
  17.178                  a = flag for abstracting over function occurences
  17.179                  i = subgoal  *)
  17.180  
  17.181 @@ -289,18 +288,18 @@
  17.182      val (t,np,nh) = prepare_for_presburger sg q g'
  17.183      (* Some simpsets for dealing with mod div abs and nat*)
  17.184      val mod_div_simpset = Simplifier.theory_context sg HOL_basic_ss
  17.185 -			addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, 
  17.186 -				  nat_mod_add_right_eq, int_mod_add_eq, 
  17.187 -				  int_mod_add_right_eq, int_mod_add_left_eq,
  17.188 -				  nat_div_add_eq, int_div_add_eq,
  17.189 -				  mod_self, zmod_self,
  17.190 -				  DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
  17.191 -				  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
  17.192 -				  zdiv_zero,zmod_zero,div_0,mod_0,
  17.193 -				  zdiv_1,zmod_1,div_1,mod_1,
  17.194 -				  Suc_plus1]
  17.195 -			addsimps add_ac
  17.196 -			addsimprocs [cancel_div_mod_proc]
  17.197 +                        addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq,
  17.198 +                                  nat_mod_add_right_eq, int_mod_add_eq,
  17.199 +                                  int_mod_add_right_eq, int_mod_add_left_eq,
  17.200 +                                  nat_div_add_eq, int_div_add_eq,
  17.201 +                                  mod_self, zmod_self,
  17.202 +                                  DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
  17.203 +                                  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
  17.204 +                                  zdiv_zero,zmod_zero,div_0,mod_0,
  17.205 +                                  zdiv_1,zmod_1,div_1,mod_1,
  17.206 +                                  Suc_plus1]
  17.207 +                        addsimps add_ac
  17.208 +                        addsimprocs [cancel_div_mod_proc]
  17.209      val simpset0 = HOL_basic_ss
  17.210        addsimps [mod_div_equality', Suc_plus1]
  17.211        addsimps comp_arith
  17.212 @@ -328,47 +327,43 @@
  17.213      (* The result of the quantifier elimination *)
  17.214      val (th, tac) = case (prop_of pre_thm) of
  17.215          Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
  17.216 -    let val pth = 
  17.217 +    let val pth =
  17.218            (* If quick_and_dirty then run without proof generation as oracle*)
  17.219 -             if !quick_and_dirty 
  17.220 +             if !quick_and_dirty
  17.221               then presburger_oracle sg (Pattern.eta_long [] t1)
  17.222  (*
  17.223 -assume (cterm_of sg 
  17.224 -	       (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
  17.225 +assume (cterm_of sg
  17.226 +               (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
  17.227  *)
  17.228 -	     else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
  17.229 -    in 
  17.230 +             else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
  17.231 +    in
  17.232            (trace_msg ("calling procedure with term:\n" ^
  17.233               Sign.string_of_term sg t1);
  17.234             ((pth RS iffD2) RS pre_thm,
  17.235              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
  17.236      end
  17.237        | _ => (pre_thm, assm_tac i)
  17.238 -  in (rtac (((mp_step nh) o (spec_step np)) th) i 
  17.239 +  in (rtac (((mp_step nh) o (spec_step np)) th) i
  17.240        THEN tac) st
  17.241    end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st);
  17.242  
  17.243 -fun presburger_args meth =
  17.244 - let val parse_flag = 
  17.245 +val presburger_meth =
  17.246 + let val parse_flag =
  17.247           Args.$$$ "no_quantify" >> K (apfst (K false))
  17.248        || Args.$$$ "no_abs" >> K (apsnd (K false));
  17.249   in
  17.250 -   Method.simple_args 
  17.251 -  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
  17.252 -    curry (Library.foldl op |>) (true, true))
  17.253 -    (fn (q,a) => fn _ => meth q a 1)
  17.254 +   Method.simple_args
  17.255 +     (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
  17.256 +      curry (Library.foldl op |>) (true, true))
  17.257 +     (fn (q,a) => K (Method.SIMPLE_METHOD' (presburger_tac q a)))
  17.258    end;
  17.259  
  17.260 -fun presburger_method q a i = Method.METHOD (fn facts =>
  17.261 -  Method.insert_tac facts 1 THEN presburger_tac q a i)
  17.262 -
  17.263  val presburger_arith_tac = mk_arith_tactic "presburger" (fn i => fn st =>
  17.264    (warning "Trying full Presburger arithmetic ...";
  17.265     presburger_tac true true i st));
  17.266  
  17.267  val setup =
  17.268 -  Method.add_method ("presburger",
  17.269 -    presburger_args presburger_method,
  17.270 +  Method.add_method ("presburger", presburger_meth,
  17.271      "decision procedure for Presburger arithmetic") #>
  17.272    arith_tactic_add presburger_arith_tac;
  17.273  
    18.1 --- a/src/HOL/Isar_examples/Hoare.thy	Wed Nov 29 15:44:46 2006 +0100
    18.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Wed Nov 29 15:44:51 2006 +0100
    18.3 @@ -447,7 +447,7 @@
    18.4  
    18.5  method_setup hoare = {*
    18.6    Method.no_args
    18.7 -    (Method.SIMPLE_METHOD' HEADGOAL 
    18.8 +    (Method.SIMPLE_METHOD'
    18.9         (hoare_tac (simp_tac (HOL_basic_ss addsimps [thm "Record.K_record_apply"] )))) *}
   18.10    "verification condition generator for Hoare logic"
   18.11  
    19.1 --- a/src/HOL/Library/comm_ring.ML	Wed Nov 29 15:44:46 2006 +0100
    19.2 +++ b/src/HOL/Library/comm_ring.ML	Wed Nov 29 15:44:51 2006 +0100
    19.3 @@ -127,7 +127,7 @@
    19.4    end);
    19.5  
    19.6  val comm_ring_meth =
    19.7 -  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' HEADGOAL (comm_ring_tac ctxt));
    19.8 +  Method.ctxt_args (Method.SIMPLE_METHOD' o comm_ring_tac);
    19.9  
   19.10  val setup =
   19.11    Method.add_method ("comm_ring", comm_ring_meth,
    20.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed Nov 29 15:44:46 2006 +0100
    20.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Nov 29 15:44:51 2006 +0100
    20.3 @@ -332,7 +332,7 @@
    20.4  
    20.5  fun simp_meth_setup tac =
    20.6    Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
    20.7 -  (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
    20.8 +  (Method.SIMPLE_METHOD' o tac o local_simpset_of);
    20.9  
   20.10  val perm_eq_meth            = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
   20.11  val perm_eq_meth_debug      = simp_meth_setup (perm_simp_tac DEBUG_tac);
    21.1 --- a/src/HOL/Prolog/HOHH.thy	Wed Nov 29 15:44:46 2006 +0100
    21.2 +++ b/src/HOL/Prolog/HOHH.thy	Wed Nov 29 15:44:51 2006 +0100
    21.3 @@ -11,7 +11,7 @@
    21.4  begin
    21.5  
    21.6  method_setup ptac =
    21.7 -  {* Method.thms_args (Method.SIMPLE_METHOD' HEADGOAL o Prolog.ptac) *}
    21.8 +  {* Method.thms_args (Method.SIMPLE_METHOD' o Prolog.ptac) *}
    21.9    "Basic Lambda Prolog interpreter"
   21.10  
   21.11  method_setup prolog =
    22.1 --- a/src/HOL/Real/ferrante_rackoff.ML	Wed Nov 29 15:44:46 2006 +0100
    22.2 +++ b/src/HOL/Real/ferrante_rackoff.ML	Wed Nov 29 15:44:51 2006 +0100
    22.3 @@ -69,9 +69,9 @@
    22.4  fun spec_step n th = if n = 0 then th else spec_step (n - 1) th RS spec ;
    22.5  fun mp_step n th = if n = 0 then th else mp_step (n - 1) th RS mp;
    22.6  
    22.7 -local
    22.8 -  val context_ss = simpset_of (the_context ())
    22.9 -in fun ferrack_tac q i =  ObjectLogic.atomize_tac i
   22.10 +val context_ss = simpset_of (the_context ());
   22.11 +
   22.12 +fun ferrack_tac q i =  ObjectLogic.atomize_tac i
   22.13    THEN REPEAT_DETERM (split_tac [split_min, split_max,abs_split] i)
   22.14    THEN (fn st =>
   22.15    let
   22.16 @@ -103,21 +103,19 @@
   22.17    in (rtac (((mp_step nh) o (spec_step np)) th) i 
   22.18        THEN tac) st
   22.19    end handle Subscript => no_tac st | Ferrante_Rackoff_Proof.FAILURE _ => no_tac st);
   22.20 -end; (*local*)
   22.21  
   22.22 -fun ferrack_args meth =
   22.23 - let
   22.24 -   val parse_flag =  Args.$$$ "no_quantify" >> (K (K false));
   22.25 - in
   22.26 -   Method.simple_args 
   22.27 -  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
   22.28 -    curry (Library.foldl op |>) true)
   22.29 -    (fn q => fn _ => meth q 1)
   22.30 +val ferrack_meth =
   22.31 +  let
   22.32 +    val parse_flag =  Args.$$$ "no_quantify" >> (K (K false));
   22.33 +  in
   22.34 +    Method.simple_args 
   22.35 +      (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
   22.36 +        curry (Library.foldl op |>) true)
   22.37 +      (fn q => K (Method.SIMPLE_METHOD' (ferrack_tac q)))
   22.38    end;
   22.39  
   22.40  val setup =
   22.41 -  Method.add_method ("ferrack",
   22.42 -     ferrack_args (Method.SIMPLE_METHOD oo ferrack_tac),
   22.43 -     "LCF-proof-producing decision procedure for linear real arithmetic");
   22.44 +  Method.add_method ("ferrack", ferrack_meth,
   22.45 +    "LCF-proof-producing decision procedure for linear real arithmetic");
   22.46  
   22.47 -end
   22.48 +end;
    23.1 --- a/src/HOL/SAT.thy	Wed Nov 29 15:44:46 2006 +0100
    23.2 +++ b/src/HOL/SAT.thy	Wed Nov 29 15:44:51 2006 +0100
    23.3 @@ -17,7 +17,7 @@
    23.4  begin
    23.5  
    23.6  text {* \medskip Late package setup: default values for refute, see
    23.7 -  also theory @{text Refute}. *}
    23.8 +  also theory @{theory Refute}. *}
    23.9  
   23.10  refute_params
   23.11   ["itself"=1,
   23.12 @@ -30,10 +30,10 @@
   23.13  
   23.14  ML {* structure sat = SATFunc(structure cnf = cnf); *}
   23.15  
   23.16 -method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD (sat.sat_tac 1)) *}
   23.17 +method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *}
   23.18    "SAT solver"
   23.19  
   23.20 -method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD (sat.satx_tac 1)) *}
   23.21 +method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD' sat.satx_tac) *}
   23.22    "SAT solver (with definitional CNF)"
   23.23  
   23.24  end
    24.1 --- a/src/HOL/SET-Protocol/EventSET.thy	Wed Nov 29 15:44:46 2006 +0100
    24.2 +++ b/src/HOL/SET-Protocol/EventSET.thy	Wed Nov 29 15:44:51 2006 +0100
    24.3 @@ -188,8 +188,7 @@
    24.4  *}
    24.5  
    24.6  method_setup analz_mono_contra = {*
    24.7 -    Method.no_args
    24.8 -      (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
    24.9 +    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
   24.10      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
   24.11  
   24.12  end
    25.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Wed Nov 29 15:44:46 2006 +0100
    25.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Wed Nov 29 15:44:51 2006 +0100
    25.3 @@ -935,21 +935,17 @@
    25.4  
    25.5  method_setup spy_analz = {*
    25.6      Method.ctxt_args (fn ctxt =>
    25.7 -        Method.METHOD (fn facts =>
    25.8 -            gen_spy_analz_tac (local_clasimpset_of ctxt) 1))*}
    25.9 +        Method.SIMPLE_METHOD' (gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
   25.10      "for proving the Fake case when analz is involved"
   25.11  
   25.12  method_setup atomic_spy_analz = {*
   25.13      Method.ctxt_args (fn ctxt =>
   25.14 -        Method.METHOD (fn facts =>
   25.15 -            atomic_spy_analz_tac (local_clasimpset_of ctxt) 1))*}
   25.16 +        Method.SIMPLE_METHOD' (atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
   25.17      "for debugging spy_analz"
   25.18  
   25.19  method_setup Fake_insert_simp = {*
   25.20      Method.ctxt_args (fn ctxt =>
   25.21 -        Method.METHOD (fn facts =>
   25.22 -            Fake_insert_simp_tac (local_simpset_of ctxt) 1))*}
   25.23 +        Method.SIMPLE_METHOD' (Fake_insert_simp_tac (local_simpset_of ctxt))) *}
   25.24      "for debugging spy_analz"
   25.25  
   25.26 -
   25.27  end
    26.1 --- a/src/HOL/SET-Protocol/PublicSET.thy	Wed Nov 29 15:44:46 2006 +0100
    26.2 +++ b/src/HOL/SET-Protocol/PublicSET.thy	Wed Nov 29 15:44:51 2006 +0100
    26.3 @@ -373,8 +373,7 @@
    26.4  
    26.5  method_setup possibility = {*
    26.6      Method.ctxt_args (fn ctxt =>
    26.7 -        Method.METHOD (fn facts =>
    26.8 -            gen_possibility_tac (local_simpset_of ctxt))) *}
    26.9 +        Method.SIMPLE_METHOD (gen_possibility_tac (local_simpset_of ctxt))) *}
   26.10      "for proving possibility theorems"
   26.11  
   26.12  
    27.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Wed Nov 29 15:44:46 2006 +0100
    27.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Wed Nov 29 15:44:51 2006 +0100
    27.3 @@ -10,10 +10,9 @@
    27.4  call the procedure with the parameter abs.
    27.5  *)
    27.6  
    27.7 -signature PRESBURGER = 
    27.8 +signature PRESBURGER =
    27.9  sig
   27.10   val presburger_tac : bool -> bool -> int -> tactic
   27.11 - val presburger_method : bool -> bool -> int -> Proof.method
   27.12   val setup : theory -> theory
   27.13   val trace : bool ref
   27.14  end;
   27.15 @@ -25,7 +24,7 @@
   27.16  fun trace_msg s = if !trace then tracing s else ();
   27.17  
   27.18  (*-----------------------------------------------------------------*)
   27.19 -(*cooper_pp: provefunction for the one-exstance quantifier elimination*)
   27.20 +(*cooper_pp: provefunction for the one-existance quantifier elimination*)
   27.21  (* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
   27.22  (*-----------------------------------------------------------------*)
   27.23  
   27.24 @@ -36,35 +35,35 @@
   27.25   "pred_Pls","pred_Min","pred_1","pred_0",
   27.26    "succ_Pls", "succ_Min", "succ_1", "succ_0",
   27.27    "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
   27.28 -  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1", 
   27.29 -  "minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0", 
   27.30 +  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1",
   27.31 +  "minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0",
   27.32    "add_Pls_right", "add_Min_right"];
   27.33 - val intarithrel = 
   27.34 -     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
   27.35 -		"int_le_number_of_eq","int_iszero_number_of_0",
   27.36 -		"int_less_number_of_eq_neg"]) @
   27.37 -     (map (fn s => thm s RS thm "lift_bool") 
   27.38 -	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
   27.39 -	   "int_neg_number_of_Min"])@
   27.40 -     (map (fn s => thm s RS thm "nlift_bool") 
   27.41 -	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
   27.42 -     
   27.43 + val intarithrel =
   27.44 +     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT",
   27.45 +                "int_le_number_of_eq","int_iszero_number_of_0",
   27.46 +                "int_less_number_of_eq_neg"]) @
   27.47 +     (map (fn s => thm s RS thm "lift_bool")
   27.48 +          ["int_iszero_number_of_Pls","int_iszero_number_of_1",
   27.49 +           "int_neg_number_of_Min"])@
   27.50 +     (map (fn s => thm s RS thm "nlift_bool")
   27.51 +          ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
   27.52 +
   27.53  val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
   27.54 -			"int_number_of_diff_sym", "int_number_of_mult_sym"];
   27.55 +                        "int_number_of_diff_sym", "int_number_of_mult_sym"];
   27.56  val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
   27.57 -			"mult_nat_number_of", "eq_nat_number_of",
   27.58 -			"less_nat_number_of"]
   27.59 -val powerarith = 
   27.60 -    (map thm ["nat_number_of", "zpower_number_of_even", 
   27.61 -	      "zpower_Pls", "zpower_Min"]) @ 
   27.62 -    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
   27.63 -			   thm "one_eq_Numeral1_nring"] 
   27.64 +                        "mult_nat_number_of", "eq_nat_number_of",
   27.65 +                        "less_nat_number_of"]
   27.66 +val powerarith =
   27.67 +    (map thm ["nat_number_of", "zpower_number_of_even",
   27.68 +              "zpower_Pls", "zpower_Min"]) @
   27.69 +    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring",
   27.70 +                           thm "one_eq_Numeral1_nring"]
   27.71    (thm "zpower_number_of_odd"))]
   27.72  
   27.73 -val comp_arith = binarith @ intarith @ intarithrel @ natarith 
   27.74 -	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
   27.75 +val comp_arith = binarith @ intarith @ intarithrel @ natarith
   27.76 +            @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
   27.77  
   27.78 -fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
   27.79 +fun cooper_pp sg (fm as e$Abs(xn,xT,p)) =
   27.80    let val (xn1,p1) = Syntax.variant_abs (xn,xT,p)
   27.81    in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
   27.82  
   27.83 @@ -140,7 +139,7 @@
   27.84     ("Divides.mod", iT --> iT --> iT),
   27.85     ("HOL.plus", iT --> iT --> iT),
   27.86     ("HOL.minus", iT --> iT --> iT),
   27.87 -   ("HOL.times", iT --> iT --> iT), 
   27.88 +   ("HOL.times", iT --> iT --> iT),
   27.89     ("HOL.abs", iT --> iT),
   27.90     ("HOL.uminus", iT --> iT),
   27.91     ("HOL.max", iT --> iT --> iT),
   27.92 @@ -154,7 +153,7 @@
   27.93     ("Divides.mod", nT --> nT --> nT),
   27.94     ("HOL.plus", nT --> nT --> nT),
   27.95     ("HOL.minus", nT --> nT --> nT),
   27.96 -   ("HOL.times", nT --> nT --> nT), 
   27.97 +   ("HOL.times", nT --> nT --> nT),
   27.98     ("Suc", nT --> nT),
   27.99     ("HOL.max", nT --> nT --> nT),
  27.100     ("HOL.min", nT --> nT --> nT),
  27.101 @@ -186,12 +185,12 @@
  27.102  
  27.103  fun getfuncs fm = case strip_comb fm of
  27.104      (Free (_, T), ts as _ :: _) =>
  27.105 -      if body_type T mem [iT, nT] 
  27.106 -         andalso not (ts = []) andalso forall (null o loose_bnos) ts 
  27.107 +      if body_type T mem [iT, nT]
  27.108 +         andalso not (ts = []) andalso forall (null o loose_bnos) ts
  27.109        then [fm]
  27.110        else Library.foldl op union ([], map getfuncs ts)
  27.111    | (Var (_, T), ts as _ :: _) =>
  27.112 -      if body_type T mem [iT, nT] 
  27.113 +      if body_type T mem [iT, nT]
  27.114           andalso not (ts = []) andalso forall (null o loose_bnos) ts then [fm]
  27.115        else Library.foldl op union ([], map getfuncs ts)
  27.116    | (Const (s, T), ts) =>
  27.117 @@ -202,7 +201,7 @@
  27.118    | _ => [];
  27.119  
  27.120  
  27.121 -fun abstract_pres sg fm = 
  27.122 +fun abstract_pres sg fm =
  27.123    foldr (fn (t, u) =>
  27.124        let val T = fastype_of t
  27.125        in all T $ Abs ("x", T, abstract_over (t, u)) end)
  27.126 @@ -214,11 +213,11 @@
  27.127   It returns true if there is a subterm coresponding to the application of
  27.128   a function on a bounded variable.
  27.129  
  27.130 - Function applications are allowed only for well predefined functions a 
  27.131 + Function applications are allowed only for well predefined functions a
  27.132   consts*)
  27.133  
  27.134  fun has_free_funcs fm  = case strip_comb fm of
  27.135 -    (Free (_, T), ts as _ :: _) => 
  27.136 +    (Free (_, T), ts as _ :: _) =>
  27.137        if (body_type T mem [iT,nT]) andalso (not (T mem [iT,nT]))
  27.138        then true
  27.139        else exists (fn x => x) (map has_free_funcs ts)
  27.140 @@ -233,24 +232,24 @@
  27.141  
  27.142  (*returns true if the formula is relevant for presburger arithmetic tactic
  27.143  The constants occuring in term t should be a subset of the allowed_consts
  27.144 - There also should be no occurences of application of functions on bounded 
  27.145 - variables. Whenever this function will be used, it will be ensured that t 
  27.146 - will not contain subterms with function symbols that could have been 
  27.147 + There also should be no occurences of application of functions on bounded
  27.148 + variables. Whenever this function will be used, it will be ensured that t
  27.149 + will not contain subterms with function symbols that could have been
  27.150   abstracted over.*)
  27.151 - 
  27.152 -fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso 
  27.153 +
  27.154 +fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso
  27.155    map (fn i => snd (List.nth (ps, i))) (loose_bnos t) @
  27.156    map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
  27.157    subset [iT, nT]
  27.158    andalso not (has_free_funcs t);
  27.159  
  27.160  
  27.161 -fun prepare_for_presburger sg q fm = 
  27.162 +fun prepare_for_presburger sg q fm =
  27.163    let
  27.164      val ps = Logic.strip_params fm
  27.165      val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
  27.166      val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
  27.167 -    val _ = if relevant (rev ps) c then () 
  27.168 +    val _ = if relevant (rev ps) c then ()
  27.169                 else  (trace_msg ("Conclusion is not a presburger term:\n" ^
  27.170               Sign.string_of_term sg c); raise CooperDec.COOPER)
  27.171      fun mk_all ((s, T), (P,n)) =
  27.172 @@ -275,7 +274,7 @@
  27.173  
  27.174  (* the presburger tactic*)
  27.175  
  27.176 -(* Parameters : q = flag for quantify ofer free variables ; 
  27.177 +(* Parameters : q = flag for quantify ofer free variables ;
  27.178                  a = flag for abstracting over function occurences
  27.179                  i = subgoal  *)
  27.180  
  27.181 @@ -289,18 +288,18 @@
  27.182      val (t,np,nh) = prepare_for_presburger sg q g'
  27.183      (* Some simpsets for dealing with mod div abs and nat*)
  27.184      val mod_div_simpset = Simplifier.theory_context sg HOL_basic_ss
  27.185 -			addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, 
  27.186 -				  nat_mod_add_right_eq, int_mod_add_eq, 
  27.187 -				  int_mod_add_right_eq, int_mod_add_left_eq,
  27.188 -				  nat_div_add_eq, int_div_add_eq,
  27.189 -				  mod_self, zmod_self,
  27.190 -				  DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
  27.191 -				  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
  27.192 -				  zdiv_zero,zmod_zero,div_0,mod_0,
  27.193 -				  zdiv_1,zmod_1,div_1,mod_1,
  27.194 -				  Suc_plus1]
  27.195 -			addsimps add_ac
  27.196 -			addsimprocs [cancel_div_mod_proc]
  27.197 +                        addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq,
  27.198 +                                  nat_mod_add_right_eq, int_mod_add_eq,
  27.199 +                                  int_mod_add_right_eq, int_mod_add_left_eq,
  27.200 +                                  nat_div_add_eq, int_div_add_eq,
  27.201 +                                  mod_self, zmod_self,
  27.202 +                                  DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
  27.203 +                                  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
  27.204 +                                  zdiv_zero,zmod_zero,div_0,mod_0,
  27.205 +                                  zdiv_1,zmod_1,div_1,mod_1,
  27.206 +                                  Suc_plus1]
  27.207 +                        addsimps add_ac
  27.208 +                        addsimprocs [cancel_div_mod_proc]
  27.209      val simpset0 = HOL_basic_ss
  27.210        addsimps [mod_div_equality', Suc_plus1]
  27.211        addsimps comp_arith
  27.212 @@ -328,47 +327,43 @@
  27.213      (* The result of the quantifier elimination *)
  27.214      val (th, tac) = case (prop_of pre_thm) of
  27.215          Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
  27.216 -    let val pth = 
  27.217 +    let val pth =
  27.218            (* If quick_and_dirty then run without proof generation as oracle*)
  27.219 -             if !quick_and_dirty 
  27.220 +             if !quick_and_dirty
  27.221               then presburger_oracle sg (Pattern.eta_long [] t1)
  27.222  (*
  27.223 -assume (cterm_of sg 
  27.224 -	       (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
  27.225 +assume (cterm_of sg
  27.226 +               (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
  27.227  *)
  27.228 -	     else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
  27.229 -    in 
  27.230 +             else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
  27.231 +    in
  27.232            (trace_msg ("calling procedure with term:\n" ^
  27.233               Sign.string_of_term sg t1);
  27.234             ((pth RS iffD2) RS pre_thm,
  27.235              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
  27.236      end
  27.237        | _ => (pre_thm, assm_tac i)
  27.238 -  in (rtac (((mp_step nh) o (spec_step np)) th) i 
  27.239 +  in (rtac (((mp_step nh) o (spec_step np)) th) i
  27.240        THEN tac) st
  27.241    end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st);
  27.242  
  27.243 -fun presburger_args meth =
  27.244 - let val parse_flag = 
  27.245 +val presburger_meth =
  27.246 + let val parse_flag =
  27.247           Args.$$$ "no_quantify" >> K (apfst (K false))
  27.248        || Args.$$$ "no_abs" >> K (apsnd (K false));
  27.249   in
  27.250 -   Method.simple_args 
  27.251 -  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
  27.252 -    curry (Library.foldl op |>) (true, true))
  27.253 -    (fn (q,a) => fn _ => meth q a 1)
  27.254 +   Method.simple_args
  27.255 +     (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
  27.256 +      curry (Library.foldl op |>) (true, true))
  27.257 +     (fn (q,a) => K (Method.SIMPLE_METHOD' (presburger_tac q a)))
  27.258    end;
  27.259  
  27.260 -fun presburger_method q a i = Method.METHOD (fn facts =>
  27.261 -  Method.insert_tac facts 1 THEN presburger_tac q a i)
  27.262 -
  27.263  val presburger_arith_tac = mk_arith_tactic "presburger" (fn i => fn st =>
  27.264    (warning "Trying full Presburger arithmetic ...";
  27.265     presburger_tac true true i st));
  27.266  
  27.267  val setup =
  27.268 -  Method.add_method ("presburger",
  27.269 -    presburger_args presburger_method,
  27.270 +  Method.add_method ("presburger", presburger_meth,
  27.271      "decision procedure for Presburger arithmetic") #>
  27.272    arith_tactic_add presburger_arith_tac;
  27.273  
    28.1 --- a/src/HOL/Tools/function_package/auto_term.ML	Wed Nov 29 15:44:46 2006 +0100
    28.2 +++ b/src/HOL/Tools/function_package/auto_term.ML	Wed Nov 29 15:44:51 2006 +0100
    28.3 @@ -6,34 +6,33 @@
    28.4  Method "relation" to commence a termination proof using a user-specified relation.
    28.5  *)
    28.6  
    28.7 -
    28.8  signature FUNDEF_RELATION =
    28.9  sig
   28.10 -  val relation_meth : Proof.context -> term -> Method.method
   28.11 -
   28.12 +  val relation_tac: Proof.context -> term -> int -> tactic
   28.13    val setup: theory -> theory
   28.14  end
   28.15  
   28.16  structure FundefRelation : FUNDEF_RELATION =
   28.17  struct
   28.18  
   28.19 -fun relation_meth ctxt rel = 
   28.20 +fun relation_tac ctxt rel =
   28.21      let
   28.22        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
   28.23 -                 
   28.24 +
   28.25        val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
   28.26        val rule = FundefCommon.get_termination_rule ctxt |> the
   28.27                    |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1)
   28.28 -          
   28.29 +
   28.30        val prem = #1 (Logic.dest_implies (Thm.prop_of rule))
   28.31        val Rvar = cert (Var (the_single (Term.add_vars prem [])))
   28.32 -    in
   28.33 -      Method.SIMPLE_METHOD (rtac (Drule.cterm_instantiate [(Rvar, rel')] rule) 1)
   28.34 -    end
   28.35 -   
   28.36 +    in rtac (Drule.cterm_instantiate [(Rvar, rel')] rule) end
   28.37 +
   28.38 +fun relation_meth src =
   28.39 +  Method.syntax Args.term src
   28.40 +  #> (fn (ctxt, rel) => Method.SIMPLE_METHOD' (relation_tac ctxt rel))
   28.41  
   28.42  val setup = Method.add_methods
   28.43 -  [("relation", uncurry relation_meth oo Method.syntax Args.term,
   28.44 +  [("relation", relation_meth,
   28.45      "proves termination using a user-specified wellfounded relation")]
   28.46  
   28.47  end
    29.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Nov 29 15:44:46 2006 +0100
    29.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Nov 29 15:44:51 2006 +0100
    29.3 @@ -161,20 +161,20 @@
    29.4      handle COMPLETENESS => Seq.empty
    29.5  
    29.6  
    29.7 -val pat_completeness = Method.SIMPLE_METHOD (pat_complete_tac 1)
    29.8 +val pat_completeness = Method.SIMPLE_METHOD' pat_complete_tac
    29.9  
   29.10  val by_pat_completeness_simp =
   29.11      Proof.global_terminal_proof
   29.12        (Method.Basic (K pat_completeness),
   29.13 -       SOME (Method.Source (Args.src (("simp_all", []), Position.none))))
   29.14 -         (* FIXME avoid dynamic scoping of method name! *)
   29.15 +       SOME (Method.Source_i (Args.src (("HOL.simp_all", []), Position.none))))
   29.16  
   29.17  fun termination_by_lexicographic_order name =
   29.18      FundefPackage.setup_termination_proof (SOME name)
   29.19      #> Proof.global_terminal_proof (Method.Basic LexicographicOrder.lexicographic_order, NONE)
   29.20  
   29.21  val setup =
   29.22 -    Method.add_methods [("pat_completeness", Method.no_args pat_completeness, "Completeness prover for datatype patterns")]
   29.23 +    Method.add_methods [("pat_completeness", Method.no_args pat_completeness,
   29.24 +      "Completeness prover for datatype patterns")]
   29.25  
   29.26  
   29.27  
    30.1 --- a/src/HOL/Tools/meson.ML	Wed Nov 29 15:44:46 2006 +0100
    30.2 +++ b/src/HOL/Tools/meson.ML	Wed Nov 29 15:44:51 2006 +0100
    30.3 @@ -666,15 +666,11 @@
    30.4  
    30.5  (*No CHANGED_PROP here, since these always appear in the preamble*)
    30.6  
    30.7 -val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac;
    30.8 -
    30.9 -val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
   30.10 -
   30.11  val skolemize_setup =
   30.12    Method.add_methods
   30.13 -    [("skolemize", Method.no_args skolemize_meth, 
   30.14 +    [("skolemize", Method.no_args (Method.SIMPLE_METHOD' skolemize_tac),
   30.15        "Skolemization into existential quantifiers"),
   30.16 -     ("make_clauses", Method.no_args make_clauses_meth, 
   30.17 +     ("make_clauses", Method.no_args (Method.SIMPLE_METHOD' make_clauses_tac), 
   30.18        "Conversion to !!-quantified meta-level clauses")];
   30.19  
   30.20  end;
    31.1 --- a/src/HOL/Tools/res_atp.ML	Wed Nov 29 15:44:46 2006 +0100
    31.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Nov 29 15:44:51 2006 +0100
    31.3 @@ -15,7 +15,7 @@
    31.4    val problem_name: string ref
    31.5    val time_limit: int ref
    31.6    val set_prover: string -> unit
    31.7 -   
    31.8 +
    31.9    datatype mode = Auto | Fol | Hol
   31.10    val linkup_logic_mode : mode ref
   31.11    val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
   31.12 @@ -65,22 +65,22 @@
   31.13  (********************************************************************)
   31.14  
   31.15  (*** background linkup ***)
   31.16 -val call_atp = ref false; 
   31.17 +val call_atp = ref false;
   31.18  val hook_count = ref 0;
   31.19  val time_limit = ref 60;
   31.20 -val prover = ref "";   
   31.21 +val prover = ref "";
   31.22  
   31.23 -fun set_prover atp = 
   31.24 +fun set_prover atp =
   31.25    case String.map Char.toLower atp of
   31.26 -      "e" => 
   31.27 +      "e" =>
   31.28            (ReduceAxiomsN.max_new := 100;
   31.29             ReduceAxiomsN.theory_const := false;
   31.30             prover := "E")
   31.31 -    | "spass" => 
   31.32 +    | "spass" =>
   31.33            (ReduceAxiomsN.max_new := 40;
   31.34             ReduceAxiomsN.theory_const := true;
   31.35             prover := "spass")
   31.36 -    | "vampire" => 
   31.37 +    | "vampire" =>
   31.38            (ReduceAxiomsN.max_new := 60;
   31.39             ReduceAxiomsN.theory_const := false;
   31.40             prover := "vampire")
   31.41 @@ -94,17 +94,17 @@
   31.42  val problem_name = ref "prob";
   31.43  
   31.44  (*Return the path to a "helper" like SPASS or tptp2X, first checking that
   31.45 -  it exists.  FIXME: modify to use Path primitives and move to some central place.*)  
   31.46 +  it exists.  FIXME: modify to use Path primitives and move to some central place.*)
   31.47  fun helper_path evar base =
   31.48    case getenv evar of
   31.49        "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
   31.50 -    | home => 
   31.51 +    | home =>
   31.52          let val path = home ^ "/" ^ base
   31.53 -        in  if File.exists (File.unpack_platform_path path) then path 
   31.54 -	    else error ("Could not find the file " ^ path)
   31.55 -	end;  
   31.56 +        in  if File.exists (File.unpack_platform_path path) then path
   31.57 +            else error ("Could not find the file " ^ path)
   31.58 +        end;
   31.59  
   31.60 -fun probfile_nosuffix _ = 
   31.61 +fun probfile_nosuffix _ =
   31.62    if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
   31.63    else if File.exists (File.unpack_platform_path (!destdir))
   31.64    then !destdir ^ "/" ^ !problem_name
   31.65 @@ -118,15 +118,15 @@
   31.66  val eprover_time = ref 60;
   31.67  val spass_time = ref 60;
   31.68  
   31.69 -fun run_vampire time =  
   31.70 +fun run_vampire time =
   31.71      if (time >0) then vampire_time:= time
   31.72      else vampire_time:=60;
   31.73  
   31.74 -fun run_eprover time = 
   31.75 +fun run_eprover time =
   31.76      if (time > 0) then eprover_time:= time
   31.77      else eprover_time:=60;
   31.78  
   31.79 -fun run_spass time = 
   31.80 +fun run_spass time =
   31.81      if (time > 0) then spass_time:=time
   31.82      else spass_time:=60;
   31.83  
   31.84 @@ -141,24 +141,24 @@
   31.85  val hol_const_types_only = ResHolClause.const_types_only;
   31.86  val hol_no_types = ResHolClause.no_types;
   31.87  fun hol_typ_level () = ResHolClause.find_typ_level ();
   31.88 -fun is_typed_hol () = 
   31.89 +fun is_typed_hol () =
   31.90      let val tp_level = hol_typ_level()
   31.91      in
   31.92 -	not (tp_level = ResHolClause.T_NONE)
   31.93 +        not (tp_level = ResHolClause.T_NONE)
   31.94      end;
   31.95  
   31.96  fun atp_input_file () =
   31.97 -    let val file = !problem_name 
   31.98 +    let val file = !problem_name
   31.99      in
  31.100 -	if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
  31.101 -	else if File.exists (File.unpack_platform_path (!destdir))
  31.102 -	then !destdir ^ "/" ^ file
  31.103 -	else error ("No such directory: " ^ !destdir)
  31.104 +        if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
  31.105 +        else if File.exists (File.unpack_platform_path (!destdir))
  31.106 +        then !destdir ^ "/" ^ file
  31.107 +        else error ("No such directory: " ^ !destdir)
  31.108      end;
  31.109  
  31.110  val include_all = ref true;
  31.111  val include_simpset = ref false;
  31.112 -val include_claset = ref false; 
  31.113 +val include_claset = ref false;
  31.114  val include_atpset = ref true;
  31.115  
  31.116  (*Tests show that follow_defs gives VERY poor results with "include_all"*)
  31.117 @@ -200,7 +200,7 @@
  31.118  fun upgrade_lg HOLC _ = HOLC
  31.119    | upgrade_lg HOL HOLC = HOLC
  31.120    | upgrade_lg HOL _ = HOL
  31.121 -  | upgrade_lg FOL lg = lg; 
  31.122 +  | upgrade_lg FOL lg = lg;
  31.123  
  31.124  (* check types *)
  31.125  fun has_bool_hfn (Type("bool",_)) = true
  31.126 @@ -211,34 +211,34 @@
  31.127  fun is_hol_fn tp =
  31.128      let val (targs,tr) = strip_type tp
  31.129      in
  31.130 -	exists (has_bool_hfn) (tr::targs)
  31.131 +        exists (has_bool_hfn) (tr::targs)
  31.132      end;
  31.133  
  31.134  fun is_hol_pred tp =
  31.135      let val (targs,tr) = strip_type tp
  31.136      in
  31.137 -	exists (has_bool_hfn) targs
  31.138 +        exists (has_bool_hfn) targs
  31.139      end;
  31.140  
  31.141  exception FN_LG of term;
  31.142  
  31.143 -fun fn_lg (t as Const(f,tp)) (lg,seen) = 
  31.144 -    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
  31.145 -  | fn_lg (t as Free(f,tp)) (lg,seen) = 
  31.146 -    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
  31.147 +fun fn_lg (t as Const(f,tp)) (lg,seen) =
  31.148 +    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen)
  31.149 +  | fn_lg (t as Free(f,tp)) (lg,seen) =
  31.150 +    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen)
  31.151    | fn_lg (t as Var(f,tp)) (lg,seen) =
  31.152      if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen)
  31.153    | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen)
  31.154 -  | fn_lg f _ = raise FN_LG(f); 
  31.155 +  | fn_lg f _ = raise FN_LG(f);
  31.156  
  31.157  
  31.158  fun term_lg [] (lg,seen) = (lg,seen)
  31.159    | term_lg (tm::tms) (FOL,seen) =
  31.160        let val (f,args) = strip_comb tm
  31.161 -	  val (lg',seen') = if f mem seen then (FOL,seen) 
  31.162 -			    else fn_lg f (FOL,seen)
  31.163 +          val (lg',seen') = if f mem seen then (FOL,seen)
  31.164 +                            else fn_lg f (FOL,seen)
  31.165        in
  31.166 -	if is_fol_logic lg' then ()
  31.167 +        if is_fol_logic lg' then ()
  31.168          else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f);
  31.169          term_lg (args@tms) (lg',seen')
  31.170        end
  31.171 @@ -246,11 +246,11 @@
  31.172  
  31.173  exception PRED_LG of term;
  31.174  
  31.175 -fun pred_lg (t as Const(P,tp)) (lg,seen)= 
  31.176 -      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) 
  31.177 -      else (lg,insert (op =) t seen) 
  31.178 +fun pred_lg (t as Const(P,tp)) (lg,seen)=
  31.179 +      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen)
  31.180 +      else (lg,insert (op =) t seen)
  31.181    | pred_lg (t as Free(P,tp)) (lg,seen) =
  31.182 -      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) 
  31.183 +      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen)
  31.184        else (lg,insert (op =) t seen)
  31.185    | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
  31.186    | pred_lg P _ = raise PRED_LG(P);
  31.187 @@ -259,21 +259,21 @@
  31.188  fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
  31.189    | lit_lg P (lg,seen) =
  31.190        let val (pred,args) = strip_comb P
  31.191 -	  val (lg',seen') = if pred mem seen then (lg,seen) 
  31.192 -			    else pred_lg pred (lg,seen)
  31.193 +          val (lg',seen') = if pred mem seen then (lg,seen)
  31.194 +                            else pred_lg pred (lg,seen)
  31.195        in
  31.196 -	if is_fol_logic lg' then ()
  31.197 -	else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred);
  31.198 -	term_lg args (lg',seen')
  31.199 +        if is_fol_logic lg' then ()
  31.200 +        else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred);
  31.201 +        term_lg args (lg',seen')
  31.202        end;
  31.203  
  31.204  fun lits_lg [] (lg,seen) = (lg,seen)
  31.205    | lits_lg (lit::lits) (FOL,seen) =
  31.206        let val (lg,seen') = lit_lg lit (FOL,seen)
  31.207        in
  31.208 -	if is_fol_logic lg then ()
  31.209 -	else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit);
  31.210 -	lits_lg lits (lg,seen')
  31.211 +        if is_fol_logic lg then ()
  31.212 +        else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit);
  31.213 +        lits_lg lits (lg,seen')
  31.214        end
  31.215    | lits_lg lits (lg,seen) = (lg,seen);
  31.216  
  31.217 @@ -288,18 +288,18 @@
  31.218  fun logic_of_clauses [] (lg,seen) = (lg,seen)
  31.219    | logic_of_clauses (cls::clss) (FOL,seen) =
  31.220      let val (lg,seen') = logic_of_clause cls (FOL,seen)
  31.221 -	val _ =
  31.222 +        val _ =
  31.223            if is_fol_logic lg then ()
  31.224            else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
  31.225      in
  31.226 -	logic_of_clauses clss (lg,seen')
  31.227 +        logic_of_clauses clss (lg,seen')
  31.228      end
  31.229    | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
  31.230  
  31.231  fun problem_logic_goals_aux [] (lg,seen) = lg
  31.232 -  | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
  31.233 +  | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) =
  31.234      problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
  31.235 -    
  31.236 +
  31.237  fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
  31.238  
  31.239  fun is_fol_thms ths = ((fst(logic_of_clauses (map prop_of ths) (FOL,[]))) = FOL);
  31.240 @@ -311,9 +311,9 @@
  31.241  (*** white list and black list of lemmas ***)
  31.242  
  31.243  (*The rule subsetI is frequently omitted by the relevance filter.*)
  31.244 -val whitelist = ref [subsetI]; 
  31.245 -  
  31.246 -(*Names of theorems (not theorem lists! See multi_blacklist below) to be banned. 
  31.247 +val whitelist = ref [subsetI];
  31.248 +
  31.249 +(*Names of theorems (not theorem lists! See multi_blacklist below) to be banned.
  31.250  
  31.251    These theorems typically produce clauses that are prolific (match too many equality or
  31.252    membership literals) and relate to seldom-used facts. Some duplicate other rules.
  31.253 @@ -447,7 +447,7 @@
  31.254  
  31.255  
  31.256  (*These might be prolific but are probably OK, and min and max are basic.
  31.257 -   "Orderings.max_less_iff_conj", 
  31.258 +   "Orderings.max_less_iff_conj",
  31.259     "Orderings.min_less_iff_conj",
  31.260     "Orderings.min_max.below_inf.below_inf_conv",
  31.261     "Orderings.min_max.below_sup.above_sup_conv",
  31.262 @@ -463,25 +463,25 @@
  31.263  exception HASH_CLAUSE and HASH_STRING;
  31.264  
  31.265  (*Catches (for deletion) theorems automatically generated from other theorems*)
  31.266 -fun insert_suffixed_names ht x = 
  31.267 -     (Polyhash.insert ht (x^"_iff1", ()); 
  31.268 -      Polyhash.insert ht (x^"_iff2", ()); 
  31.269 -      Polyhash.insert ht (x^"_dest", ())); 
  31.270 +fun insert_suffixed_names ht x =
  31.271 +     (Polyhash.insert ht (x^"_iff1", ());
  31.272 +      Polyhash.insert ht (x^"_iff2", ());
  31.273 +      Polyhash.insert ht (x^"_dest", ()));
  31.274  
  31.275  (*Reject theorems with names like "List.filter.filter_list_def" or
  31.276    "Accessible_Part.acc.defs", as these are definitions arising from packages.
  31.277    FIXME: this will also block definitions within locales*)
  31.278  fun is_package_def a =
  31.279 -   length (NameSpace.unpack a) > 2 andalso 
  31.280 +   length (NameSpace.unpack a) > 2 andalso
  31.281     String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a;
  31.282  
  31.283 -fun make_banned_test xs = 
  31.284 +fun make_banned_test xs =
  31.285    let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
  31.286                                  (6000, HASH_STRING)
  31.287 -      fun banned s = 
  31.288 +      fun banned s =
  31.289              isSome (Polyhash.peek ht s) orelse is_package_def s
  31.290    in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
  31.291 -      app (insert_suffixed_names ht) (!blacklist @ xs); 
  31.292 +      app (insert_suffixed_names ht) (!blacklist @ xs);
  31.293        banned
  31.294    end;
  31.295  
  31.296 @@ -509,40 +509,40 @@
  31.297  
  31.298  (*Use a hash table to eliminate duplicates from xs. Argument is a list of
  31.299    (thm * (string * int)) tuples. The theorems are hashed into the table. *)
  31.300 -fun make_unique xs = 
  31.301 +fun make_unique xs =
  31.302    let val ht = mk_clause_table 7000
  31.303    in
  31.304        Output.debug("make_unique gets " ^ Int.toString (length xs) ^ " clauses");
  31.305 -      app (ignore o Polyhash.peekInsert ht) xs;  
  31.306 +      app (ignore o Polyhash.peekInsert ht) xs;
  31.307        Polyhash.listItems ht
  31.308    end;
  31.309  
  31.310  (*Remove existing axiom clauses from the conjecture clauses, as this can dramatically
  31.311    boost an ATP's performance (for some reason)*)
  31.312 -fun subtract_cls c_clauses ax_clauses = 
  31.313 +fun subtract_cls c_clauses ax_clauses =
  31.314    let val ht = mk_clause_table 2200
  31.315        fun known x = isSome (Polyhash.peek ht x)
  31.316    in
  31.317 -      app (ignore o Polyhash.peekInsert ht) ax_clauses;  
  31.318 -      filter (not o known) c_clauses 
  31.319 +      app (ignore o Polyhash.peekInsert ht) ax_clauses;
  31.320 +      filter (not o known) c_clauses
  31.321    end;
  31.322  
  31.323 -(*Filter axiom clauses, but keep supplied clauses and clauses in whitelist. 
  31.324 +(*Filter axiom clauses, but keep supplied clauses and clauses in whitelist.
  31.325    Duplicates are removed later.*)
  31.326  fun get_relevant_clauses thy cls_thms white_cls goals =
  31.327    white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
  31.328  
  31.329  fun display_thms [] = ()
  31.330 -  | display_thms ((name,thm)::nthms) = 
  31.331 +  | display_thms ((name,thm)::nthms) =
  31.332        let val nthm = name ^ ": " ^ (string_of_thm thm)
  31.333        in Output.debug nthm; display_thms nthms  end;
  31.334 - 
  31.335 +
  31.336  fun all_valid_thms ctxt =
  31.337    PureThy.thms_containing (ProofContext.theory_of ctxt) ([], []) @
  31.338    filter (ProofContext.valid_thms ctxt)
  31.339      (FactIndex.find (ProofContext.fact_index_of ctxt) ([], []));
  31.340  
  31.341 -fun multi_name a (th, (n,pairs)) = 
  31.342 +fun multi_name a (th, (n,pairs)) =
  31.343    (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
  31.344  
  31.345  fun add_multi_names_aux ((a, []), pairs) = pairs
  31.346 @@ -557,7 +557,7 @@
  31.347    ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
  31.348  
  31.349  (*Ignore blacklisted theorem lists*)
  31.350 -fun add_multi_names ((a, ths), pairs) = 
  31.351 +fun add_multi_names ((a, ths), pairs) =
  31.352    if a mem_string multi_blacklist orelse (Sign.base_name a) mem_string multi_base_blacklist
  31.353    then pairs
  31.354    else add_multi_names_aux ((a, ths), pairs);
  31.355 @@ -565,7 +565,7 @@
  31.356  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
  31.357  
  31.358  (*The single theorems go BEFORE the multiple ones*)
  31.359 -fun name_thm_pairs ctxt = 
  31.360 +fun name_thm_pairs ctxt =
  31.361    let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
  31.362    in  foldl add_multi_names (foldl add_multi_names [] mults) singles  end;
  31.363  
  31.364 @@ -573,40 +573,40 @@
  31.365    | check_named (_,th) = true;
  31.366  
  31.367  (* get lemmas from claset, simpset, atpset and extra supplied rules *)
  31.368 -fun get_clasimp_atp_lemmas ctxt user_thms = 
  31.369 +fun get_clasimp_atp_lemmas ctxt user_thms =
  31.370    let val included_thms =
  31.371 -	if !include_all 
  31.372 -	then (tap (fn ths => Output.debug
  31.373 -	             ("Including all " ^ Int.toString (length ths) ^ " theorems")) 
  31.374 -	          (name_thm_pairs ctxt))
  31.375 -	else 
  31.376 -	let val claset_thms =
  31.377 -		if !include_claset then ResAxioms.claset_rules_of ctxt
  31.378 -		else []
  31.379 -	    val simpset_thms = 
  31.380 -		if !include_simpset then ResAxioms.simpset_rules_of ctxt
  31.381 -		else []
  31.382 -	    val atpset_thms =
  31.383 -		if !include_atpset then ResAxioms.atpset_rules_of ctxt
  31.384 -		else []
  31.385 -	    val _ = if !Output.show_debug_msgs 
  31.386 -		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
  31.387 -		    else ()		 
  31.388 -	in  claset_thms @ simpset_thms @ atpset_thms  end
  31.389 -      val user_rules = filter check_named 
  31.390 +        if !include_all
  31.391 +        then (tap (fn ths => Output.debug
  31.392 +                     ("Including all " ^ Int.toString (length ths) ^ " theorems"))
  31.393 +                  (name_thm_pairs ctxt))
  31.394 +        else
  31.395 +        let val claset_thms =
  31.396 +                if !include_claset then ResAxioms.claset_rules_of ctxt
  31.397 +                else []
  31.398 +            val simpset_thms =
  31.399 +                if !include_simpset then ResAxioms.simpset_rules_of ctxt
  31.400 +                else []
  31.401 +            val atpset_thms =
  31.402 +                if !include_atpset then ResAxioms.atpset_rules_of ctxt
  31.403 +                else []
  31.404 +            val _ = if !Output.show_debug_msgs
  31.405 +                    then (Output.debug "ATP theorems: "; display_thms atpset_thms)
  31.406 +                    else ()
  31.407 +        in  claset_thms @ simpset_thms @ atpset_thms  end
  31.408 +      val user_rules = filter check_named
  31.409                           (map (ResAxioms.pairname)
  31.410 -			   (if null user_thms then !whitelist else user_thms))
  31.411 +                           (if null user_thms then !whitelist else user_thms))
  31.412    in
  31.413        (filter check_named included_thms, user_rules)
  31.414    end;
  31.415  
  31.416  (*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
  31.417 -fun blacklist_filter ths = 
  31.418 -  if !run_blacklist_filter then 
  31.419 +fun blacklist_filter ths =
  31.420 +  if !run_blacklist_filter then
  31.421        let val _ = Output.debug("blacklist filter gets " ^ Int.toString (length ths) ^ " theorems")
  31.422            val banned = make_banned_test (map #1 ths)
  31.423 -	  fun ok (a,_) = not (banned a)
  31.424 -	  val okthms = filter ok ths
  31.425 +          fun ok (a,_) = not (banned a)
  31.426 +          val okthms = filter ok ths
  31.427            val _ = Output.debug("...and returns " ^ Int.toString (length okthms))
  31.428        in  okthms end
  31.429    else ths;
  31.430 @@ -653,7 +653,7 @@
  31.431  (* ATP invocation methods setup                                *)
  31.432  (***************************************************************)
  31.433  
  31.434 -fun cnf_hyps_thms ctxt = 
  31.435 +fun cnf_hyps_thms ctxt =
  31.436      let val ths = Assumption.prems_of ctxt
  31.437      in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
  31.438  
  31.439 @@ -664,15 +664,15 @@
  31.440  
  31.441  (*Ensures that no higher-order theorems "leak out"*)
  31.442  fun restrict_to_logic logic cls =
  31.443 -  if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
  31.444 -	                else cls;
  31.445 +  if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls
  31.446 +                        else cls;
  31.447  
  31.448  (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
  31.449  
  31.450  (** Too general means, positive equality literal with a variable X as one operand,
  31.451    when X does not occur properly in the other operand. This rules out clearly
  31.452    inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
  31.453 - 
  31.454 +
  31.455  fun occurs ix =
  31.456      let fun occ(Var (jx,_)) = (ix=jx)
  31.457            | occ(t1$t2)      = occ t1 orelse occ t2
  31.458 @@ -685,7 +685,7 @@
  31.459  (*Unwanted equalities include
  31.460    (1) those between a variable that does not properly occur in the second operand,
  31.461    (2) those between a variable and a record, since these seem to be prolific "cases" thms
  31.462 -*)  
  31.463 +*)
  31.464  fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
  31.465    | too_general_eqterms _ = false;
  31.466  
  31.467 @@ -698,7 +698,7 @@
  31.468    | is_taut _ = false;
  31.469  
  31.470  (*True if the term contains a variable whose (atomic) type is in the given list.*)
  31.471 -fun has_typed_var tycons = 
  31.472 +fun has_typed_var tycons =
  31.473    let fun var_tycon (Var (_, Type(a,_))) = a mem_string tycons
  31.474          | var_tycon _ = false
  31.475    in  exists var_tycon o term_vars  end;
  31.476 @@ -713,72 +713,67 @@
  31.477    filter (not o unwanted o prop_of o fst) cls;
  31.478  
  31.479  fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
  31.480 -    if is_fol_logic logic 
  31.481 +    if is_fol_logic logic
  31.482      then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
  31.483      else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
  31.484  
  31.485  fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas =
  31.486 -    if is_fol_logic logic 
  31.487 +    if is_fol_logic logic
  31.488      then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
  31.489      else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas;
  31.490  
  31.491  (*Called by the oracle-based methods declared in res_atp_methods.ML*)
  31.492  fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
  31.493 -    let val conj_cls = make_clauses conjectures 
  31.494 +    let val conj_cls = make_clauses conjectures
  31.495                           |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
  31.496 -	val hyp_cls = cnf_hyps_thms ctxt
  31.497 -	val goal_cls = conj_cls@hyp_cls
  31.498 -	val goal_tms = map prop_of goal_cls
  31.499 -	val logic = case mode of 
  31.500 +        val hyp_cls = cnf_hyps_thms ctxt
  31.501 +        val goal_cls = conj_cls@hyp_cls
  31.502 +        val goal_tms = map prop_of goal_cls
  31.503 +        val logic = case mode of
  31.504                              Auto => problem_logic_goals [goal_tms]
  31.505 -			  | Fol => FOL
  31.506 -			  | Hol => HOL
  31.507 -	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
  31.508 -	val cla_simp_atp_clauses = included_thms |> blacklist_filter
  31.509 -	                             |> ResAxioms.cnf_rules_pairs |> make_unique 
  31.510 -                                     |> restrict_to_logic logic 
  31.511 +                          | Fol => FOL
  31.512 +                          | Hol => HOL
  31.513 +        val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
  31.514 +        val cla_simp_atp_clauses = included_thms |> blacklist_filter
  31.515 +                                     |> ResAxioms.cnf_rules_pairs |> make_unique
  31.516 +                                     |> restrict_to_logic logic
  31.517                                       |> remove_unwanted_clauses
  31.518 -	val user_cls = ResAxioms.cnf_rules_pairs user_rules
  31.519 -	val thy = ProofContext.theory_of ctxt
  31.520 -	val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
  31.521 -	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
  31.522 +        val user_cls = ResAxioms.cnf_rules_pairs user_rules
  31.523 +        val thy = ProofContext.theory_of ctxt
  31.524 +        val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
  31.525 +        val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
  31.526          val subs = tfree_classes_of_terms goal_tms
  31.527          and axtms = map (prop_of o #1) axclauses
  31.528          val supers = tvar_classes_of_terms axtms
  31.529          and tycons = type_consts_of_terms thy (goal_tms@axtms)
  31.530          (*TFrees in conjecture clauses; TVars in axiom clauses*)
  31.531 -        val classrel_clauses = 
  31.532 +        val classrel_clauses =
  31.533                if keep_types then ResClause.make_classrel_clauses thy subs supers
  31.534                else []
  31.535 -	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers else []
  31.536 -        val writer = if dfg then dfg_writer else tptp_writer 
  31.537 -	and file = atp_input_file()
  31.538 -	and user_lemmas_names = map #1 user_rules
  31.539 +        val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers else []
  31.540 +        val writer = if dfg then dfg_writer else tptp_writer
  31.541 +        and file = atp_input_file()
  31.542 +        and user_lemmas_names = map #1 user_rules
  31.543      in
  31.544 -	writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
  31.545 -	Output.debug ("Writing to " ^ file);
  31.546 -	file
  31.547 +        writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
  31.548 +        Output.debug ("Writing to " ^ file);
  31.549 +        file
  31.550      end;
  31.551  
  31.552  
  31.553  (**** remove tmp files ****)
  31.554 -fun cond_rm_tmp file = 
  31.555 -    if !Output.show_debug_msgs orelse !destdir <> "" then Output.debug "ATP input kept..." 
  31.556 +fun cond_rm_tmp file =
  31.557 +    if !Output.show_debug_msgs orelse !destdir <> "" then Output.debug "ATP input kept..."
  31.558      else OS.FileSys.remove file;
  31.559  
  31.560  
  31.561  (****** setup ATPs as Isabelle methods ******)
  31.562 -fun atp_meth' tac ths ctxt = 
  31.563 -    Method.SIMPLE_METHOD' HEADGOAL
  31.564 -    (tac ctxt ths);
  31.565  
  31.566 -fun atp_meth tac ths ctxt = 
  31.567 +fun atp_meth tac ths ctxt =
  31.568      let val thy = ProofContext.theory_of ctxt
  31.569 -	val _ = ResClause.init thy
  31.570 -	val _ = ResHolClause.init thy
  31.571 -    in
  31.572 -	atp_meth' tac ths ctxt
  31.573 -    end;
  31.574 +        val _ = ResClause.init thy
  31.575 +        val _ = ResHolClause.init thy
  31.576 +    in Method.SIMPLE_METHOD' (tac ctxt ths) end;
  31.577  
  31.578  fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
  31.579  
  31.580 @@ -802,25 +797,25 @@
  31.581                let val spass = helper_path "SPASS_HOME" "SPASS"
  31.582                    val sopts =
  31.583     "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
  31.584 -              in 
  31.585 +              in
  31.586                    ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
  31.587                end
  31.588              else if !prover = "vampire"
  31.589 -	    then 
  31.590 +            then
  31.591                let val vampire = helper_path "VAMPIRE_HOME" "vampire"
  31.592                    val vopts = "--mode casc%-t " ^ time  (*what about -m 100000?*)
  31.593                in
  31.594                    ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
  31.595                end
  31.596 -      	     else if !prover = "E"
  31.597 -      	     then
  31.598 -	       let val Eprover = helper_path "E_HOME" "eproof"
  31.599 -	       in
  31.600 -		  ("E", Eprover, 
  31.601 -		     "--tstp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
  31.602 -		   make_atp_list xs (n+1)
  31.603 -	       end
  31.604 -	     else error ("Invalid prover name: " ^ !prover)
  31.605 +             else if !prover = "E"
  31.606 +             then
  31.607 +               let val Eprover = helper_path "E_HOME" "eproof"
  31.608 +               in
  31.609 +                  ("E", Eprover,
  31.610 +                     "--tstp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
  31.611 +                   make_atp_list xs (n+1)
  31.612 +               end
  31.613 +             else error ("Invalid prover name: " ^ !prover)
  31.614            end
  31.615  
  31.616      val atp_list = make_atp_list sg_terms 1
  31.617 @@ -828,7 +823,7 @@
  31.618      Watcher.callResProvers(childout,atp_list);
  31.619      Output.debug "Sent commands to watcher!"
  31.620    end
  31.621 -  
  31.622 +
  31.623  fun trace_array fname =
  31.624    let val path = File.unpack_platform_path fname
  31.625    in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
  31.626 @@ -839,7 +834,7 @@
  31.627        val st = Seq.hd (EVERY' tacs n th)
  31.628        val negs = Option.valOf (metahyps_thms n st)
  31.629    in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end;
  31.630 -		                       
  31.631 +
  31.632  (*We write out problem files for each subgoal. Argument probfile generates filenames,
  31.633    and allows the suppression of the suffix "_1" in problem-generation mode.
  31.634    FIXME: does not cope with &&, and it isn't easy because one could have multiple
  31.635 @@ -852,12 +847,12 @@
  31.636          | get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1)
  31.637        val goal_cls = get_neg_subgoals goals 1
  31.638        val logic = case !linkup_logic_mode of
  31.639 -		Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
  31.640 -	      | Fol => FOL
  31.641 -	      | Hol => HOL
  31.642 +                Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
  31.643 +              | Fol => FOL
  31.644 +              | Hol => HOL
  31.645        val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
  31.646        val included_cls = included_thms |> blacklist_filter
  31.647 -                                       |> ResAxioms.cnf_rules_pairs |> make_unique 
  31.648 +                                       |> ResAxioms.cnf_rules_pairs |> make_unique
  31.649                                         |> restrict_to_logic logic
  31.650                                         |> remove_unwanted_clauses
  31.651        val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
  31.652 @@ -866,11 +861,11 @@
  31.653        val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls
  31.654        val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
  31.655                    axcls_list
  31.656 -      val keep_types = if is_fol_logic logic then !ResClause.keep_types 
  31.657 +      val keep_types = if is_fol_logic logic then !ResClause.keep_types
  31.658                         else is_typed_hol ()
  31.659 -      val writer = if !prover = "spass" then dfg_writer else tptp_writer 
  31.660 +      val writer = if !prover = "spass" then dfg_writer else tptp_writer
  31.661        fun write_all [] [] _ = []
  31.662 -	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
  31.663 +        | write_all (ccls::ccls_list) (axcls::axcls_list) k =
  31.664              let val fname = probfile k
  31.665                  val axcls = make_unique axcls
  31.666                  val ccls = subtract_cls ccls axcls
  31.667 @@ -880,7 +875,7 @@
  31.668                  and supers = tvar_classes_of_terms axtms
  31.669                  and tycons = type_consts_of_terms thy (ccltms@axtms)
  31.670                  (*TFrees in conjecture clauses; TVars in axiom clauses*)
  31.671 -                val classrel_clauses = 
  31.672 +                val classrel_clauses =
  31.673                        if keep_types then ResClause.make_classrel_clauses thy subs supers
  31.674                        else []
  31.675                  val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
  31.676 @@ -889,7 +884,7 @@
  31.677                  val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
  31.678                  val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
  31.679                  val thm_names = Array.fromList clnames
  31.680 -                val _ = if !Output.show_debug_msgs 
  31.681 +                val _ = if !Output.show_debug_msgs
  31.682                          then trace_array (fname ^ "_thm_names") thm_names else ()
  31.683              in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
  31.684        val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
  31.685 @@ -897,16 +892,16 @@
  31.686        (filenames, thm_names_list)
  31.687    end;
  31.688  
  31.689 -val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
  31.690 +val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream *
  31.691                                      Posix.Process.pid * string list) option);
  31.692  
  31.693  fun kill_last_watcher () =
  31.694 -    (case !last_watcher_pid of 
  31.695 +    (case !last_watcher_pid of
  31.696           NONE => ()
  31.697 -       | SOME (_, _, pid, files) => 
  31.698 -	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
  31.699 -	   Watcher.killWatcher pid;  
  31.700 -	   ignore (map (try cond_rm_tmp) files)))
  31.701 +       | SOME (_, _, pid, files) =>
  31.702 +          (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
  31.703 +           Watcher.killWatcher pid;
  31.704 +           ignore (map (try cond_rm_tmp) files)))
  31.705       handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
  31.706  
  31.707  (*writes out the current clasimpset to a tptp file;
  31.708 @@ -920,7 +915,7 @@
  31.709        val (childin, childout, pid) = Watcher.createWatcher (th, thm_names_list)
  31.710      in
  31.711        last_watcher_pid := SOME (childin, childout, pid, files);
  31.712 -      Output.debug ("problem files: " ^ space_implode ", " files); 
  31.713 +      Output.debug ("problem files: " ^ space_implode ", " files);
  31.714        Output.debug ("pid: " ^ string_of_pid pid);
  31.715        watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
  31.716      end;
  31.717 @@ -928,17 +923,17 @@
  31.718  val isar_atp = setmp print_mode [] isar_atp_body;
  31.719  
  31.720  (*For ML scripts, and primarily, for debugging*)
  31.721 -fun callatp () = 
  31.722 +fun callatp () =
  31.723    let val th = topthm()
  31.724        val ctxt = ProofContext.init (theory_of_thm th)
  31.725    in  isar_atp_body (ctxt, th)  end;
  31.726  
  31.727 -val isar_atp_writeonly = setmp print_mode [] 
  31.728 +val isar_atp_writeonly = setmp print_mode []
  31.729        (fn (ctxt,th) =>
  31.730         if Thm.no_prems th then ()
  31.731 -       else 
  31.732 -         let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
  31.733 -          	            else prob_pathname
  31.734 +       else
  31.735 +         let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix
  31.736 +                            else prob_pathname
  31.737           in ignore (write_problem_files probfile (ctxt,th)) end);
  31.738  
  31.739  
  31.740 @@ -947,9 +942,9 @@
  31.741  fun invoke_atp_ml (ctxt, goal) =
  31.742    let val thy = ProofContext.theory_of ctxt;
  31.743    in
  31.744 -    Output.debug ("subgoals in isar_atp:\n" ^ 
  31.745 -		  Pretty.string_of (ProofContext.pretty_term ctxt
  31.746 -		    (Logic.mk_conjunction_list (Thm.prems_of goal))));
  31.747 +    Output.debug ("subgoals in isar_atp:\n" ^
  31.748 +                  Pretty.string_of (ProofContext.pretty_term ctxt
  31.749 +                    (Logic.mk_conjunction_list (Thm.prems_of goal))));
  31.750      Output.debug ("current theory: " ^ Context.theory_name thy);
  31.751      inc hook_count;
  31.752      Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
  31.753 @@ -965,9 +960,9 @@
  31.754    in  invoke_atp_ml (ctxt, goal)  end);
  31.755  
  31.756  val call_atpP =
  31.757 -  OuterSyntax.command 
  31.758 -    "ProofGeneral.call_atp" 
  31.759 -    "call automatic theorem provers" 
  31.760 +  OuterSyntax.command
  31.761 +    "ProofGeneral.call_atp"
  31.762 +    "call automatic theorem provers"
  31.763      OuterKeyword.diag
  31.764      (Scan.succeed invoke_atp);
  31.765  
    32.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Nov 29 15:44:46 2006 +0100
    32.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Nov 29 15:44:51 2006 +0100
    32.3 @@ -608,14 +608,10 @@
    32.4  
    32.5  fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths);
    32.6  
    32.7 -fun meson_meth ths ctxt =
    32.8 -  Method.SIMPLE_METHOD' HEADGOAL
    32.9 -    (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs);
   32.10 -
   32.11 -val meson_method_setup =
   32.12 -  Method.add_methods
   32.13 -    [("meson", Method.thms_ctxt_args meson_meth,
   32.14 -      "MESON resolution proof procedure")];
   32.15 +val meson_method_setup = Method.add_methods
   32.16 +  [("meson", Method.thms_args (fn ths =>
   32.17 +      Method.SIMPLE_METHOD' (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs)),
   32.18 +    "MESON resolution proof procedure")];
   32.19  
   32.20  (** Attribute for converting a theorem into clauses **)
   32.21  
    33.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Wed Nov 29 15:44:46 2006 +0100
    33.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Wed Nov 29 15:44:51 2006 +0100
    33.3 @@ -129,8 +129,7 @@
    33.4  
    33.5  method_setup ns_induct = {*
    33.6      Method.ctxt_args (fn ctxt =>
    33.7 -        Method.METHOD (fn facts =>
    33.8 -            ns_induct_tac (local_clasimpset_of ctxt) 1)) *}
    33.9 +        Method.SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
   33.10      "for inductive reasoning about the Needham-Schroeder protocol"
   33.11  
   33.12  text{*Converts invariants into statements about reachable states*}
    34.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Wed Nov 29 15:44:46 2006 +0100
    34.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Wed Nov 29 15:44:51 2006 +0100
    34.3 @@ -11,13 +11,12 @@
    34.4  
    34.5  method_setup safety = {*
    34.6      Method.ctxt_args (fn ctxt =>
    34.7 -        Method.METHOD (fn facts => 
    34.8 -            gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
    34.9 +        Method.SIMPLE_METHOD' (gen_constrains_tac (local_clasimpset_of ctxt))) *}
   34.10      "for proving safety properties"
   34.11  
   34.12  method_setup ensures_tac = {*
   34.13      fn args => fn ctxt =>
   34.14 -        Method.goal_args' (Scan.lift Args.name) 
   34.15 +        Method.goal_args' (Scan.lift Args.name)
   34.16             (gen_ensures_tac (local_clasimpset_of ctxt))
   34.17             args ctxt *}
   34.18      "for proving progress properties"
    35.1 --- a/src/HOL/ex/Reflection.thy	Wed Nov 29 15:44:46 2006 +0100
    35.2 +++ b/src/HOL/ex/Reflection.thy	Wed Nov 29 15:44:51 2006 +0100
    35.3 @@ -18,14 +18,14 @@
    35.4    fn src =>
    35.5      Method.syntax (Attrib.thms --
    35.6        Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    35.7 -  (fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.genreify_tac ctxt eqs to))
    35.8 +  (fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs to))
    35.9  *} "partial automatic reification"
   35.10  
   35.11  method_setup reflection = {*
   35.12    fn src =>
   35.13      Method.syntax (Attrib.thms --
   35.14        Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
   35.15 -  (fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.reflection_tac ctxt ths to))
   35.16 +  (fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))
   35.17  *} "reflection method"
   35.18  
   35.19  end
    36.1 --- a/src/HOL/ex/SAT_Examples.thy	Wed Nov 29 15:44:46 2006 +0100
    36.2 +++ b/src/HOL/ex/SAT_Examples.thy	Wed Nov 29 15:44:51 2006 +0100
    36.3 @@ -82,7 +82,7 @@
    36.4  ML {* reset sat.trace_sat; *}
    36.5  ML {* reset quick_and_dirty; *}
    36.6  
    36.7 -method_setup rawsat = {* Method.no_args (Method.SIMPLE_METHOD (sat.rawsat_tac 1)) *}
    36.8 +method_setup rawsat = {* Method.no_args (Method.SIMPLE_METHOD' sat.rawsat_tac) *}
    36.9    "SAT solver (no preprocessing)"
   36.10  
   36.11  (* ML {* Toplevel.profiling := 1; *} *)
    37.1 --- a/src/Provers/eqsubst.ML	Wed Nov 29 15:44:46 2006 +0100
    37.2 +++ b/src/Provers/eqsubst.ML	Wed Nov 29 15:44:51 2006 +0100
    37.3 @@ -407,9 +407,7 @@
    37.4  (* inthms are the given arguments in Isar, and treated as eqstep with
    37.5     the first one, then the second etc *)
    37.6  fun eqsubst_meth ctxt occL inthms =
    37.7 -    Method.METHOD
    37.8 -      (fn facts =>
    37.9 -          HEADGOAL (Method.insert_tac facts THEN' eqsubst_tac ctxt occL inthms));
   37.10 +    Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
   37.11  
   37.12  (* apply a substitution inside assumption j, keeps asm in the same place *)
   37.13  fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
   37.14 @@ -523,9 +521,7 @@
   37.15  (* inthms are the given arguments in Isar, and treated as eqstep with
   37.16     the first one, then the second etc *)
   37.17  fun eqsubst_asm_meth ctxt occL inthms =
   37.18 -    Method.METHOD
   37.19 -      (fn facts =>
   37.20 -          HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac ctxt occL inthms ));
   37.21 +    Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
   37.22  
   37.23  (* syntax for options, given "(asm)" will give back true, without
   37.24     gives back false *)
    38.1 --- a/src/Provers/hypsubst.ML	Wed Nov 29 15:44:46 2006 +0100
    38.2 +++ b/src/Provers/hypsubst.ML	Wed Nov 29 15:44:51 2006 +0100
    38.3 @@ -224,18 +224,12 @@
    38.4    in CHANGED_GOAL (rtac (th' RS ssubst)) end;
    38.5  
    38.6  
    38.7 -(* proof methods *)
    38.8 -
    38.9 -val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac);
   38.10 -val hyp_subst_meth =
   38.11 -  Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac));
   38.12 -
   38.13 -
   38.14  (* theory setup *)
   38.15  
   38.16  val hypsubst_setup =
   38.17    Method.add_methods
   38.18 -    [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
   38.19 -     ("simplesubst", subst_meth, "simple substitution")];
   38.20 +    [("hypsubst", Method.no_args (Method.SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
   38.21 +        "substitution using an assumption (improper)"),
   38.22 +     ("simplesubst", Method.thm_args (Method.SIMPLE_METHOD' o stac), "simple substitution")];
   38.23  
   38.24  end;
    39.1 --- a/src/Provers/splitter.ML	Wed Nov 29 15:44:46 2006 +0100
    39.2 +++ b/src/Provers/splitter.ML	Wed Nov 29 15:44:51 2006 +0100
    39.3 @@ -477,7 +477,7 @@
    39.4  
    39.5  fun split_meth src =
    39.6    Method.syntax Attrib.thms src
    39.7 -  #> (fn (_, ths) => Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths));
    39.8 +  #> (fn (_, ths) => Method.SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths));
    39.9  
   39.10  
   39.11  (* theory setup *)
    40.1 --- a/src/Sequents/ILL.thy	Wed Nov 29 15:44:46 2006 +0100
    40.2 +++ b/src/Sequents/ILL.thy	Wed Nov 29 15:44:51 2006 +0100
    40.3 @@ -146,8 +146,8 @@
    40.4  *}
    40.5  
    40.6  method_setup best_lazy =
    40.7 -{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac lazy_cs)) *}
    40.8 -"lazy classical reasoning"
    40.9 +  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac lazy_cs)) *}
   40.10 +  "lazy classical reasoning"
   40.11  
   40.12  lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
   40.13    apply (rule derelict)
   40.14 @@ -282,10 +282,10 @@
   40.15  
   40.16  
   40.17  method_setup best_safe =
   40.18 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac safe_cs)) *} ""
   40.19 +  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac safe_cs)) *} ""
   40.20  
   40.21  method_setup best_power =
   40.22 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac power_cs)) *} ""
   40.23 +  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac power_cs)) *} ""
   40.24  
   40.25  
   40.26  (* Some examples from Troelstra and van Dalen *)
    41.1 --- a/src/Sequents/LK0.thy	Wed Nov 29 15:44:46 2006 +0100
    41.2 +++ b/src/Sequents/LK0.thy	Wed Nov 29 15:44:51 2006 +0100
    41.3 @@ -248,23 +248,23 @@
    41.4  *}
    41.5  
    41.6  method_setup fast_prop =
    41.7 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac prop_pack)) *}
    41.8 +  {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac prop_pack)) *}
    41.9    "propositional reasoning"
   41.10  
   41.11  method_setup fast =
   41.12 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac LK_pack)) *}
   41.13 +  {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_pack)) *}
   41.14    "classical reasoning"
   41.15  
   41.16  method_setup fast_dup =
   41.17 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac LK_dup_pack)) *}
   41.18 +  {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
   41.19    "classical reasoning"
   41.20  
   41.21  method_setup best =
   41.22 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac LK_pack)) *}
   41.23 +  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_pack)) *}
   41.24    "classical reasoning"
   41.25  
   41.26  method_setup best_dup =
   41.27 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac LK_dup_pack)) *}
   41.28 +  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
   41.29    "classical reasoning"
   41.30  
   41.31  
    42.1 --- a/src/ZF/UNITY/Constrains.thy	Wed Nov 29 15:44:46 2006 +0100
    42.2 +++ b/src/ZF/UNITY/Constrains.thy	Wed Nov 29 15:44:51 2006 +0100
    42.3 @@ -565,11 +565,9 @@
    42.4  *}
    42.5  
    42.6  method_setup safety = {*
    42.7 -    Method.ctxt_args (fn ctxt =>
    42.8 -        Method.METHOD (fn facts =>
    42.9 -            gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
   42.10 -    "for proving safety properties"
   42.11 +  Method.ctxt_args (fn ctxt =>
   42.12 +    Method.SIMPLE_METHOD' (gen_constrains_tac (local_clasimpset_of ctxt))) *}
   42.13 +  "for proving safety properties"
   42.14  
   42.15  
   42.16  end
   42.17 -