Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
authorwenzelm
Fri Mar 20 17:12:37 2009 +0100 (2009-03-20)
changeset 30609983e8b6e4e69
parent 30608 d9805c5b5d2e
child 30610 bcbc34cb9749
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
NEWS
src/FOL/blastdata.ML
src/FOL/simpdata.ML
src/HOL/HOL.thy
src/HOL/Tools/simpdata.ML
src/HOLCF/FOCUS/Buffer.thy
src/HOLCF/IOA/Modelcheck/Cockpit.thy
src/HOLCF/IOA/Modelcheck/MuIOA.thy
src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy
src/HOLCF/IOA/Modelcheck/Ring3.thy
src/Provers/blast.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Provers/splitter.ML
src/Pure/simplifier.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/NEWS	Fri Mar 20 17:04:44 2009 +0100
     1.2 +++ b/NEWS	Fri Mar 20 17:12:37 2009 +0100
     1.3 @@ -685,6 +685,12 @@
     1.4  Syntax.read_term_global etc.; see also OldGoals.read_term as last
     1.5  resort for legacy applications.
     1.6  
     1.7 +* Disposed old declarations, tactics, tactic combinators that refer to
     1.8 +the simpset or claset of an implicit theory (such as Addsimps,
     1.9 +Simp_tac, SIMPSET).  INCOMPATIBILITY, should use @{simpset} etc. in
    1.10 +embedded ML text, or local_simpset_of with a proper context passed as
    1.11 +explicit runtime argument.
    1.12 +
    1.13  * Antiquotations: block-structured compilation context indicated by
    1.14  \<lbrace> ... \<rbrace>; additional antiquotation forms:
    1.15  
     2.1 --- a/src/FOL/blastdata.ML	Fri Mar 20 17:04:44 2009 +0100
     2.2 +++ b/src/FOL/blastdata.ML	Fri Mar 20 17:12:37 2009 +0100
     2.3 @@ -1,5 +1,5 @@
     2.4  
     2.5 -(*** Applying BlastFun to create Blast_tac ***)
     2.6 +(*** Applying BlastFun to create blast_tac ***)
     2.7  structure Blast_Data = 
     2.8    struct
     2.9    type claset	= Cla.claset
    2.10 @@ -10,13 +10,10 @@
    2.11    val contr_tac = Cla.contr_tac
    2.12    val dup_intr	= Cla.dup_intr
    2.13    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    2.14 -  val claset	= Cla.claset
    2.15 -  val rep_cs    = Cla.rep_cs
    2.16 +  val rep_cs = Cla.rep_cs
    2.17    val cla_modifiers = Cla.cla_modifiers;
    2.18    val cla_meth' = Cla.cla_meth'
    2.19    end;
    2.20  
    2.21  structure Blast = BlastFun(Blast_Data);
    2.22 -
    2.23 -val Blast_tac = Blast.Blast_tac
    2.24 -and blast_tac = Blast.blast_tac;
    2.25 +val blast_tac = Blast.blast_tac;
     3.1 --- a/src/FOL/simpdata.ML	Fri Mar 20 17:04:44 2009 +0100
     3.2 +++ b/src/FOL/simpdata.ML	Fri Mar 20 17:12:37 2009 +0100
     3.3 @@ -117,8 +117,6 @@
     3.4  val split_asm_tac    = Splitter.split_asm_tac;
     3.5  val op addsplits     = Splitter.addsplits;
     3.6  val op delsplits     = Splitter.delsplits;
     3.7 -val Addsplits        = Splitter.Addsplits;
     3.8 -val Delsplits        = Splitter.Delsplits;
     3.9  
    3.10  
    3.11  (*** Standard simpsets ***)
     4.1 --- a/src/HOL/HOL.thy	Fri Mar 20 17:04:44 2009 +0100
     4.2 +++ b/src/HOL/HOL.thy	Fri Mar 20 17:12:37 2009 +0100
     4.3 @@ -1018,12 +1018,10 @@
     4.4    val contr_tac = Classical.contr_tac
     4.5    val dup_intr = Classical.dup_intr
     4.6    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
     4.7 -  val claset = Classical.claset
     4.8    val rep_cs = Classical.rep_cs
     4.9    val cla_modifiers = Classical.cla_modifiers
    4.10    val cla_meth' = Classical.cla_meth'
    4.11  );
    4.12 -val Blast_tac = Blast.Blast_tac;
    4.13  val blast_tac = Blast.blast_tac;
    4.14  *}
    4.15  
     5.1 --- a/src/HOL/Tools/simpdata.ML	Fri Mar 20 17:04:44 2009 +0100
     5.2 +++ b/src/HOL/Tools/simpdata.ML	Fri Mar 20 17:12:37 2009 +0100
     5.3 @@ -147,8 +147,6 @@
     5.4  
     5.5  val op addsplits     = Splitter.addsplits;
     5.6  val op delsplits     = Splitter.delsplits;
     5.7 -val Addsplits        = Splitter.Addsplits;
     5.8 -val Delsplits        = Splitter.Delsplits;
     5.9  
    5.10  
    5.11  (* integration of simplifier with classical reasoner *)
     6.1 --- a/src/HOLCF/FOCUS/Buffer.thy	Fri Mar 20 17:04:44 2009 +0100
     6.2 +++ b/src/HOLCF/FOCUS/Buffer.thy	Fri Mar 20 17:12:37 2009 +0100
     6.3 @@ -98,8 +98,11 @@
     6.4  by (erule subst, rule refl)
     6.5  
     6.6  ML {*
     6.7 -fun B_prover s tac eqs = prove_goal (the_context ()) s (fn prems => [cut_facts_tac prems 1,
     6.8 -        tac 1, auto_tac (claset(), simpset() addsimps eqs)]);
     6.9 +fun B_prover s tac eqs =
    6.10 +  let val thy = the_context () in
    6.11 +    prove_goal thy s (fn prems => [cut_facts_tac prems 1,
    6.12 +        tac 1, auto_tac (claset_of thy, simpset_of thy addsimps eqs)])
    6.13 +  end;
    6.14  
    6.15  fun prove_forw  s thm     = B_prover s (dtac (thm RS iffD1)) [];
    6.16  fun prove_backw s thm eqs = B_prover s (rtac (thm RS iffD2)) eqs;
     7.1 --- a/src/HOLCF/IOA/Modelcheck/Cockpit.thy	Fri Mar 20 17:04:44 2009 +0100
     7.2 +++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy	Fri Mar 20 17:12:37 2009 +0100
     7.3 @@ -102,18 +102,18 @@
     7.4  
     7.5  (* to prove, that info is always set at the recent alarm *)
     7.6  lemma cockpit_implements_Info_while_Al: "cockpit =<| Info_while_Al"
     7.7 -apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
     7.8 +apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
     7.9  done
    7.10  
    7.11  (* to prove that before any alarm arrives (and after each acknowledgment),
    7.12     info remains at None *)
    7.13  lemma cockpit_implements_Info_before_Al: "cockpit =<| Info_before_Al"
    7.14 -apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
    7.15 +apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
    7.16  done
    7.17  
    7.18  (* to prove that before any alarm would be acknowledged, it must be arrived *)
    7.19  lemma cockpit_implements_Al_before_Ack: "cockpit_hide =<| Al_before_Ack"
    7.20 -apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
    7.21 +apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
    7.22  apply auto
    7.23  done
    7.24  
     8.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Fri Mar 20 17:04:44 2009 +0100
     8.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Fri Mar 20 17:12:37 2009 +0100
     8.3 @@ -278,14 +278,14 @@
     8.4  by (REPEAT (rtac impI 1));
     8.5  by (REPEAT (dtac eq_reflection 1));
     8.6  (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
     8.7 -by (full_simp_tac ((simpset() delcongs (if_weak_cong :: weak_case_congs)
     8.8 +by (full_simp_tac ((simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
     8.9                                delsimps [not_iff,split_part])
    8.10  			      addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
    8.11                                          rename_simps @ ioa_simps @ asig_simps)) 1);
    8.12  by (full_simp_tac
    8.13    (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
    8.14  by (REPEAT (if_full_simp_tac
    8.15 -  (simpset() delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
    8.16 +  (simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
    8.17  by (call_mucke_tac 1);
    8.18  (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
    8.19  by (atac 1);
     9.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Fri Mar 20 17:04:44 2009 +0100
     9.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Fri Mar 20 17:12:37 2009 +0100
     9.3 @@ -18,18 +18,18 @@
     9.4  
     9.5  (* is_sim_tac makes additionally to call_sim_tac some simplifications,
     9.6  	which are suitable for implementation realtion formulas *)
     9.7 -fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) =>
     9.8 +fun is_sim_tac ss thm_list = SUBGOAL (fn (goal, i) =>
     9.9    EVERY [REPEAT (etac thin_rl i),
    9.10 -	 simp_tac (simpset() addsimps [ioa_implements_def]) i,
    9.11 +	 simp_tac (ss addsimps [ioa_implements_def]) i,
    9.12           rtac conjI i,
    9.13           rtac conjI (i+1),
    9.14  	 TRY(call_sim_tac thm_list (i+2)),
    9.15  	 TRY(atac (i+2)), 
    9.16           REPEAT(rtac refl (i+2)),
    9.17 -	 simp_tac (simpset() addsimps (thm_list @
    9.18 +	 simp_tac (ss addsimps (thm_list @
    9.19  				       comp_simps @ restrict_simps @ hide_simps @
    9.20  				       rename_simps @  ioa_simps @ asig_simps)) (i+1),
    9.21 -	 simp_tac (simpset() addsimps (thm_list @
    9.22 +	 simp_tac (ss addsimps (thm_list @
    9.23  				       comp_simps @ restrict_simps @ hide_simps @
    9.24  				       rename_simps @ ioa_simps @ asig_simps)) (i)]);
    9.25  
    10.1 --- a/src/HOLCF/IOA/Modelcheck/Ring3.thy	Fri Mar 20 17:04:44 2009 +0100
    10.2 +++ b/src/HOLCF/IOA/Modelcheck/Ring3.thy	Fri Mar 20 17:12:37 2009 +0100
    10.3 @@ -114,7 +114,7 @@
    10.4  (* property to prove: at most one (of 3) members of the ring will
    10.5  	declare itself to leader *)
    10.6  lemma at_most_one_leader: "ring =<| one_leader"
    10.7 -apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
    10.8 +apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
    10.9  apply auto
   10.10  done
   10.11  
    11.1 --- a/src/Provers/blast.ML	Fri Mar 20 17:04:44 2009 +0100
    11.2 +++ b/src/Provers/blast.ML	Fri Mar 20 17:12:37 2009 +0100
    11.3 @@ -48,7 +48,6 @@
    11.4    val contr_tac         : int -> tactic
    11.5    val dup_intr          : thm -> thm
    11.6    val hyp_subst_tac     : bool -> int -> tactic
    11.7 -  val claset            : unit -> claset
    11.8    val rep_cs    : (* dependent on classical.ML *)
    11.9        claset -> {safeIs: thm list, safeEs: thm list,
   11.10                   hazIs: thm list, hazEs: thm list,
   11.11 @@ -77,7 +76,6 @@
   11.12    val depth_tac         : claset -> int -> int -> tactic
   11.13    val depth_limit       : int Config.T
   11.14    val blast_tac         : claset -> int -> tactic
   11.15 -  val Blast_tac         : int -> tactic
   11.16    val setup             : theory -> theory
   11.17    (*debugging tools*)
   11.18    val stats             : bool ref
   11.19 @@ -89,7 +87,7 @@
   11.20    val instVars          : term -> (unit -> unit)
   11.21    val toTerm            : int -> term -> Term.term
   11.22    val readGoal          : theory -> string -> term
   11.23 -  val tryInThy          : theory -> int -> string ->
   11.24 +  val tryInThy          : theory -> claset -> int -> string ->
   11.25                    (int->tactic) list * branch list list * (int*int*exn) list
   11.26    val normBr            : branch -> branch
   11.27    end;
   11.28 @@ -1283,7 +1281,6 @@
   11.29        ((if !trace then warning ("blast: " ^ s) else ());
   11.30         Seq.empty);
   11.31  
   11.32 -fun Blast_tac i = blast_tac (Data.claset()) i;
   11.33  
   11.34  
   11.35  (*** For debugging: these apply the prover to a subgoal and return
   11.36 @@ -1294,11 +1291,11 @@
   11.37  (*Read a string to make an initial, singleton branch*)
   11.38  fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;
   11.39  
   11.40 -fun tryInThy thy lim s =
   11.41 +fun tryInThy thy cs lim s =
   11.42    let
   11.43      val state as State {fullTrace = ft, ...} = initialize thy;
   11.44      val res = timeap prove
   11.45 -      (state, start_timing(), Data.claset(), [initBranch ([readGoal thy s], lim)], I);
   11.46 +      (state, start_timing(), cs, [initBranch ([readGoal thy s], lim)], I);
   11.47      val _ = fullTrace := !ft;
   11.48    in res end;
   11.49  
    12.1 --- a/src/Provers/clasimp.ML	Fri Mar 20 17:04:44 2009 +0100
    12.2 +++ b/src/Provers/clasimp.ML	Fri Mar 20 17:12:37 2009 +0100
    12.3 @@ -26,8 +26,6 @@
    12.4    type clasimpset
    12.5    val get_css: Context.generic -> clasimpset
    12.6    val map_css: (clasimpset -> clasimpset) -> Context.generic -> Context.generic
    12.7 -  val change_clasimpset: (clasimpset -> clasimpset) -> unit
    12.8 -  val clasimpset: unit -> clasimpset
    12.9    val local_clasimpset_of: Proof.context -> clasimpset
   12.10    val addSIs2: clasimpset * thm list -> clasimpset
   12.11    val addSEs2: clasimpset * thm list -> clasimpset
   12.12 @@ -42,19 +40,10 @@
   12.13    val addss': claset * simpset -> claset
   12.14    val addIffs: clasimpset * thm list -> clasimpset
   12.15    val delIffs: clasimpset * thm list -> clasimpset
   12.16 -  val AddIffs: thm list -> unit
   12.17 -  val DelIffs: thm list -> unit
   12.18 -  val CLASIMPSET: (clasimpset -> tactic) -> tactic
   12.19 -  val CLASIMPSET': (clasimpset -> 'a -> tactic) -> 'a -> tactic
   12.20    val clarsimp_tac: clasimpset -> int -> tactic
   12.21 -  val Clarsimp_tac: int -> tactic
   12.22    val mk_auto_tac: clasimpset -> int -> int -> tactic
   12.23    val auto_tac: clasimpset -> tactic
   12.24 -  val Auto_tac: tactic
   12.25 -  val auto: unit -> unit
   12.26    val force_tac: clasimpset  -> int -> tactic
   12.27 -  val Force_tac: int -> tactic
   12.28 -  val force: int -> unit
   12.29    val fast_simp_tac: clasimpset -> int -> tactic
   12.30    val slow_simp_tac: clasimpset -> int -> tactic
   12.31    val best_simp_tac: clasimpset -> int -> tactic
   12.32 @@ -84,9 +73,6 @@
   12.33    let val (cs', ss') = f (get_css context)
   12.34    in context |> Classical.map_cs (K cs') |> Simplifier.map_ss (K ss') end;
   12.35  
   12.36 -fun change_clasimpset f = Context.>> (fn context => (Context.the_theory context; map_css f context));
   12.37 -fun clasimpset () = (Classical.claset (), Simplifier.simpset ());
   12.38 -
   12.39  fun local_clasimpset_of ctxt =
   12.40    (Classical.local_claset_of ctxt, Simplifier.local_simpset_of ctxt);
   12.41  
   12.42 @@ -168,9 +154,6 @@
   12.43                Simplifier.addsimps);
   12.44  val op delIffs = Library.foldl (delIff Classical.delrules Simplifier.delsimps);
   12.45  
   12.46 -fun AddIffs thms = change_clasimpset (fn css => css addIffs thms);
   12.47 -fun DelIffs thms = change_clasimpset (fn css => css delIffs thms);
   12.48 -
   12.49  fun addIffs_generic (x, ths) =
   12.50    Library.foldl (addIff (addXEs, addXIs) (addXEs, addXIs) #1) ((x, ()), ths) |> #1;
   12.51  
   12.52 @@ -182,19 +165,10 @@
   12.53  
   12.54  (* tacticals *)
   12.55  
   12.56 -fun CLASIMPSET tacf state =
   12.57 -  Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss))) state;
   12.58 -
   12.59 -fun CLASIMPSET' tacf i state =
   12.60 -  Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss) i)) state;
   12.61 -
   12.62 -
   12.63  fun clarsimp_tac (cs, ss) =
   12.64    safe_asm_full_simp_tac ss THEN_ALL_NEW
   12.65    Classical.clarify_tac (cs addSss ss);
   12.66  
   12.67 -fun Clarsimp_tac i = clarsimp_tac (clasimpset ()) i;
   12.68 -
   12.69  
   12.70  (* auto_tac *)
   12.71  
   12.72 @@ -231,8 +205,6 @@
   12.73      end;
   12.74  
   12.75  fun auto_tac css = mk_auto_tac css 4 2;
   12.76 -fun Auto_tac st = auto_tac (clasimpset ()) st;
   12.77 -fun auto () = by Auto_tac;
   12.78  
   12.79  
   12.80  (* force_tac *)
   12.81 @@ -242,8 +214,6 @@
   12.82          Classical.clarify_tac cs' 1,
   12.83          IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1),
   12.84          ALLGOALS (Classical.first_best_tac cs')]) end;
   12.85 -fun Force_tac i = force_tac (clasimpset ()) i;
   12.86 -fun force i = by (Force_tac i);
   12.87  
   12.88  
   12.89  (* basic combinations *)
    13.1 --- a/src/Provers/classical.ML	Fri Mar 20 17:04:44 2009 +0100
    13.2 +++ b/src/Provers/classical.ML	Fri Mar 20 17:12:37 2009 +0100
    13.3 @@ -69,11 +69,7 @@
    13.4    val appSWrappers      : claset -> wrapper
    13.5    val appWrappers       : claset -> wrapper
    13.6  
    13.7 -  val change_claset: (claset -> claset) -> unit
    13.8    val claset_of: theory -> claset
    13.9 -  val claset: unit -> claset
   13.10 -  val CLASET: (claset -> tactic) -> tactic
   13.11 -  val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic
   13.12    val local_claset_of   : Proof.context -> claset
   13.13  
   13.14    val fast_tac          : claset -> int -> tactic
   13.15 @@ -107,24 +103,6 @@
   13.16    val inst_step_tac     : claset -> int -> tactic
   13.17    val inst0_step_tac    : claset -> int -> tactic
   13.18    val instp_step_tac    : claset -> int -> tactic
   13.19 -
   13.20 -  val AddDs             : thm list -> unit
   13.21 -  val AddEs             : thm list -> unit
   13.22 -  val AddIs             : thm list -> unit
   13.23 -  val AddSDs            : thm list -> unit
   13.24 -  val AddSEs            : thm list -> unit
   13.25 -  val AddSIs            : thm list -> unit
   13.26 -  val Delrules          : thm list -> unit
   13.27 -  val Safe_tac          : tactic
   13.28 -  val Safe_step_tac     : int -> tactic
   13.29 -  val Clarify_tac       : int -> tactic
   13.30 -  val Clarify_step_tac  : int -> tactic
   13.31 -  val Step_tac          : int -> tactic
   13.32 -  val Fast_tac          : int -> tactic
   13.33 -  val Best_tac          : int -> tactic
   13.34 -  val Slow_tac          : int -> tactic
   13.35 -  val Slow_best_tac     : int -> tactic
   13.36 -  val Deepen_tac        : int -> int -> tactic
   13.37  end;
   13.38  
   13.39  signature CLASSICAL =
   13.40 @@ -870,23 +848,9 @@
   13.41  fun map_context_cs f = GlobalClaset.map (apsnd
   13.42    (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
   13.43  
   13.44 -fun change_claset f = Context.>> (Context.map_theory (map_claset f));
   13.45 -
   13.46  fun claset_of thy =
   13.47    let val (cs, ctxt_cs) = GlobalClaset.get thy
   13.48    in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
   13.49 -val claset = claset_of o ML_Context.the_global_context;
   13.50 -
   13.51 -fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
   13.52 -fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;
   13.53 -
   13.54 -fun AddDs args = change_claset (fn cs => cs addDs args);
   13.55 -fun AddEs args = change_claset (fn cs => cs addEs args);
   13.56 -fun AddIs args = change_claset (fn cs => cs addIs args);
   13.57 -fun AddSDs args = change_claset (fn cs => cs addSDs args);
   13.58 -fun AddSEs args = change_claset (fn cs => cs addSEs args);
   13.59 -fun AddSIs args = change_claset (fn cs => cs addSIs args);
   13.60 -fun Delrules args = change_claset (fn cs => cs delrules args);
   13.61  
   13.62  
   13.63  (* context dependent components *)
   13.64 @@ -930,21 +894,6 @@
   13.65  val rule_del = attrib delrule o ContextRules.rule_del;
   13.66  
   13.67  
   13.68 -(* tactics referring to the implicit claset *)
   13.69 -
   13.70 -(*the abstraction over the proof state delays the dereferencing*)
   13.71 -fun Safe_tac st           = safe_tac (claset()) st;
   13.72 -fun Safe_step_tac i st    = safe_step_tac (claset()) i st;
   13.73 -fun Clarify_step_tac i st = clarify_step_tac (claset()) i st;
   13.74 -fun Clarify_tac i st      = clarify_tac (claset()) i st;
   13.75 -fun Step_tac i st         = step_tac (claset()) i st;
   13.76 -fun Fast_tac i st         = fast_tac (claset()) i st;
   13.77 -fun Best_tac i st         = best_tac (claset()) i st;
   13.78 -fun Slow_tac i st         = slow_tac (claset()) i st;
   13.79 -fun Slow_best_tac i st    = slow_best_tac (claset()) i st;
   13.80 -fun Deepen_tac m          = deepen_tac (claset()) m;
   13.81 -
   13.82 -
   13.83  end;
   13.84  
   13.85  
   13.86 @@ -972,15 +921,12 @@
   13.87  
   13.88  (** proof methods **)
   13.89  
   13.90 -fun METHOD_CLASET tac ctxt = METHOD (tac ctxt (local_claset_of ctxt));
   13.91 -fun METHOD_CLASET' tac ctxt = METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
   13.92 -
   13.93 -
   13.94  local
   13.95  
   13.96 -fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) =>
   13.97 +fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
   13.98    let
   13.99      val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
  13.100 +    val CS {xtra_netpair, ...} = local_claset_of ctxt;
  13.101      val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
  13.102      val rules = rules1 @ rules2 @ rules3 @ rules4;
  13.103      val ruleq = Drule.multi_resolves facts rules;
  13.104 @@ -990,16 +936,15 @@
  13.105    end)
  13.106    THEN_ALL_NEW Goal.norm_hhf_tac;
  13.107  
  13.108 -fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts
  13.109 -  | rule_tac rules _ _ facts = Method.rule_tac rules facts;
  13.110 +in
  13.111  
  13.112 -fun default_tac rules ctxt cs facts =
  13.113 -  HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
  13.114 +fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
  13.115 +  | rule_tac _ rules facts = Method.rule_tac rules facts;
  13.116 +
  13.117 +fun default_tac ctxt rules facts =
  13.118 +  HEADGOAL (rule_tac ctxt rules facts) ORELSE
  13.119    Class.default_intro_tac ctxt facts;
  13.120  
  13.121 -in
  13.122 -  val rule = METHOD_CLASET' o rule_tac;
  13.123 -  val default = METHOD_CLASET o default_tac;
  13.124  end;
  13.125  
  13.126  
  13.127 @@ -1033,9 +978,11 @@
  13.128  (** setup_methods **)
  13.129  
  13.130  val setup_methods =
  13.131 -  Method.setup @{binding default} (Attrib.thms >> default)
  13.132 +  Method.setup @{binding default}
  13.133 +   (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
  13.134      "apply some intro/elim rule (potentially classical)" #>
  13.135 -  Method.setup @{binding rule} (Attrib.thms >> rule)
  13.136 +  Method.setup @{binding rule}
  13.137 +    (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
  13.138      "apply some intro/elim rule (potentially classical)" #>
  13.139    Method.setup @{binding contradiction} (Scan.succeed (K contradiction))
  13.140      "proof by contradiction" #>
    14.1 --- a/src/Provers/splitter.ML	Fri Mar 20 17:04:44 2009 +0100
    14.2 +++ b/src/Provers/splitter.ML	Fri Mar 20 17:12:37 2009 +0100
    14.3 @@ -35,8 +35,6 @@
    14.4    val split_asm_tac   : thm list -> int -> tactic
    14.5    val addsplits       : simpset * thm list -> simpset
    14.6    val delsplits       : simpset * thm list -> simpset
    14.7 -  val Addsplits       : thm list -> unit
    14.8 -  val Delsplits       : thm list -> unit
    14.9    val split_add: attribute
   14.10    val split_del: attribute
   14.11    val split_modifiers : Method.modifier parser list
   14.12 @@ -453,9 +451,6 @@
   14.13          in Simplifier.delloop (ss, split_name name asm)
   14.14    end in Library.foldl delsplit (ss,splits) end;
   14.15  
   14.16 -fun Addsplits splits = (change_simpset (fn ss => ss addsplits splits));
   14.17 -fun Delsplits splits = (change_simpset (fn ss => ss delsplits splits));
   14.18 -
   14.19  
   14.20  (* attributes *)
   14.21  
    15.1 --- a/src/Pure/simplifier.ML	Fri Mar 20 17:04:44 2009 +0100
    15.2 +++ b/src/Pure/simplifier.ML	Fri Mar 20 17:12:37 2009 +0100
    15.3 @@ -10,15 +10,8 @@
    15.4    include BASIC_META_SIMPLIFIER
    15.5    val change_simpset: (simpset -> simpset) -> unit
    15.6    val simpset_of: theory -> simpset
    15.7 -  val simpset: unit -> simpset
    15.8 -  val SIMPSET: (simpset -> tactic) -> tactic
    15.9 -  val SIMPSET': (simpset -> 'a -> tactic) -> 'a -> tactic
   15.10 -  val Addsimps: thm list -> unit
   15.11 -  val Delsimps: thm list -> unit
   15.12    val Addsimprocs: simproc list -> unit
   15.13    val Delsimprocs: simproc list -> unit
   15.14 -  val Addcongs: thm list -> unit
   15.15 -  val Delcongs: thm list -> unit
   15.16    val local_simpset_of: Proof.context -> simpset
   15.17    val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
   15.18    val safe_asm_full_simp_tac: simpset -> int -> tactic
   15.19 @@ -27,11 +20,6 @@
   15.20    val          full_simp_tac: simpset -> int -> tactic
   15.21    val        asm_lr_simp_tac: simpset -> int -> tactic
   15.22    val      asm_full_simp_tac: simpset -> int -> tactic
   15.23 -  val               Simp_tac:            int -> tactic
   15.24 -  val           Asm_simp_tac:            int -> tactic
   15.25 -  val          Full_simp_tac:            int -> tactic
   15.26 -  val        Asm_lr_simp_tac:            int -> tactic
   15.27 -  val      Asm_full_simp_tac:            int -> tactic
   15.28    val          simplify: simpset -> thm -> thm
   15.29    val      asm_simplify: simpset -> thm -> thm
   15.30    val     full_simplify: simpset -> thm -> thm
   15.31 @@ -138,17 +126,9 @@
   15.32  fun map_simpset f = Context.theory_map (map_ss f);
   15.33  fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
   15.34  fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
   15.35 -val simpset = simpset_of o ML_Context.the_global_context;
   15.36  
   15.37 -fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st;
   15.38 -fun SIMPSET' tacf i st = tacf (simpset_of (Thm.theory_of_thm st)) i st;
   15.39 -
   15.40 -fun Addsimps args = change_simpset (fn ss => ss addsimps args);
   15.41 -fun Delsimps args = change_simpset (fn ss => ss delsimps args);
   15.42  fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
   15.43  fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
   15.44 -fun Addcongs args = change_simpset (fn ss => ss addcongs args);
   15.45 -fun Delcongs args = change_simpset (fn ss => ss delcongs args);
   15.46  
   15.47  
   15.48  (* local simpset *)
   15.49 @@ -283,13 +263,6 @@
   15.50  val asm_full_simp_tac = generic_simp_tac false (true, true, true);
   15.51  val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
   15.52  
   15.53 -(*the abstraction over the proof state delays the dereferencing*)
   15.54 -fun          Simp_tac i st =          simp_tac (simpset ()) i st;
   15.55 -fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
   15.56 -fun     Full_simp_tac i st =     full_simp_tac (simpset ()) i st;
   15.57 -fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
   15.58 -fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
   15.59 -
   15.60  
   15.61  (* conversions *)
   15.62  
    16.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Mar 20 17:04:44 2009 +0100
    16.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Mar 20 17:12:37 2009 +0100
    16.3 @@ -16,7 +16,6 @@
    16.4      dom_subset : thm,                  (*inclusion of recursive set in dom*)
    16.5      intrs      : thm list,             (*introduction rules*)
    16.6      elim       : thm,                  (*case analysis theorem*)
    16.7 -    mk_cases   : string -> thm,        (*generates case theorems*)
    16.8      induct     : thm,                  (*main induction rule*)
    16.9      mutual_induct : thm};              (*mutual induction rule*)
   16.10  
   16.11 @@ -275,9 +274,6 @@
   16.12        (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ss) THEN basic_elim_tac)
   16.13        (Thm.assume A RS elim)
   16.14        |> Drule.standard';
   16.15 -  fun mk_cases a = make_cases (*delayed evaluation of body!*)
   16.16 -    (simpset ())
   16.17 -    let val thy = Thm.theory_of_thm elim in cterm_of thy (Syntax.read_prop_global thy a) end;
   16.18  
   16.19    fun induction_rules raw_induct thy =
   16.20     let
   16.21 @@ -548,7 +544,6 @@
   16.22         dom_subset = dom_subset',
   16.23         intrs = intrs'',
   16.24         elim = elim',
   16.25 -       mk_cases = mk_cases,
   16.26         induct = induct,
   16.27         mutual_induct = mutual_induct})
   16.28    end;