avoid warnings on duplicate rules in the given list;
authorwenzelm
Thu Jun 02 16:23:10 2016 +0200 (2016-06-02)
changeset 632217d43fbbaba28
parent 63220 06cbfbaf39c5
child 63222 fe92356ade42
avoid warnings on duplicate rules in the given list;
src/Pure/Isar/local_defs.ML
src/Pure/raw_simplifier.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Thu Jun 02 15:52:45 2016 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Jun 02 16:23:10 2016 +0200
     1.3 @@ -196,8 +196,8 @@
     1.4  
     1.5  fun meta_rewrite_conv ctxt =
     1.6    Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
     1.7 -    (empty_simpset ctxt
     1.8 -      addsimps (Rules.get (Context.Proof ctxt))
     1.9 +    (ctxt
    1.10 +      |> Raw_Simplifier.init_simpset (Rules.get (Context.Proof ctxt))
    1.11        |> Raw_Simplifier.add_eqcong Drule.equals_cong);    (*protect meta-level equality*)
    1.12  
    1.13  val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv;
     2.1 --- a/src/Pure/raw_simplifier.ML	Thu Jun 02 15:52:45 2016 +0200
     2.2 +++ b/src/Pure/raw_simplifier.ML	Thu Jun 02 16:23:10 2016 +0200
     2.3 @@ -90,6 +90,7 @@
     2.4    val prems_of: Proof.context -> thm list
     2.5    val add_simp: thm -> Proof.context -> Proof.context
     2.6    val del_simp: thm -> Proof.context -> Proof.context
     2.7 +  val init_simpset: thm list -> Proof.context -> Proof.context
     2.8    val add_eqcong: thm -> Proof.context -> Proof.context
     2.9    val del_eqcong: thm -> Proof.context -> Proof.context
    2.10    val add_cong: thm -> Proof.context -> Proof.context
    2.11 @@ -589,6 +590,12 @@
    2.12  
    2.13  end;
    2.14  
    2.15 +fun init_simpset thms ctxt = ctxt
    2.16 +  |> Context_Position.set_visible false
    2.17 +  |> empty_simpset
    2.18 +  |> fold add_simp thms
    2.19 +  |> Context_Position.restore_visible ctxt;
    2.20 +
    2.21  
    2.22  (* congs *)
    2.23  
    2.24 @@ -1314,8 +1321,7 @@
    2.25  
    2.26  fun rewrite _ _ [] = Thm.reflexive
    2.27    | rewrite ctxt full thms =
    2.28 -      rewrite_cterm (full, false, false) simple_prover
    2.29 -        (empty_simpset ctxt addsimps thms);
    2.30 +      rewrite_cterm (full, false, false) simple_prover (init_simpset thms ctxt);
    2.31  
    2.32  fun rewrite_rule ctxt = Conv.fconv_rule o rewrite ctxt true;
    2.33  
    2.34 @@ -1328,7 +1334,7 @@
    2.35  (*Rewrite the subgoals of a proof state (represented by a theorem)*)
    2.36  fun rewrite_goals_rule ctxt thms th =
    2.37    Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
    2.38 -    (empty_simpset ctxt addsimps thms))) th;
    2.39 +    (init_simpset thms ctxt))) th;
    2.40  
    2.41  
    2.42  (** meta-rewriting tactics **)
    2.43 @@ -1342,9 +1348,8 @@
    2.44      Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ctxt) i thm)
    2.45    else Seq.empty;
    2.46  
    2.47 -fun rewrite_goal_tac ctxt rews =
    2.48 -  generic_rewrite_goal_tac (true, false, false) (K no_tac)
    2.49 -    (empty_simpset ctxt addsimps rews);
    2.50 +fun rewrite_goal_tac ctxt thms =
    2.51 +  generic_rewrite_goal_tac (true, false, false) (K no_tac) (init_simpset thms ctxt);
    2.52  
    2.53  (*Prunes all redundant parameters from the proof state by rewriting.*)
    2.54  fun prune_params_tac ctxt = rewrite_goals_tac ctxt [Drule.triv_forall_equality];
    2.55 @@ -1387,11 +1392,15 @@
    2.56    Variable.gen_all ctxt;
    2.57  
    2.58  val hhf_ss =
    2.59 -  simpset_of (empty_simpset (Context.the_local_context ()) addsimps Drule.norm_hhf_eqs);
    2.60 +  Context.the_local_context ()
    2.61 +  |> init_simpset Drule.norm_hhf_eqs
    2.62 +  |> simpset_of;
    2.63  
    2.64  val hhf_protect_ss =
    2.65 -  simpset_of (empty_simpset (Context.the_local_context ())
    2.66 -    addsimps Drule.norm_hhf_eqs |> add_eqcong Drule.protect_cong);
    2.67 +  Context.the_local_context ()
    2.68 +  |> init_simpset Drule.norm_hhf_eqs
    2.69 +  |> add_eqcong Drule.protect_cong
    2.70 +  |> simpset_of;
    2.71  
    2.72  in
    2.73  
     3.1 --- a/src/Pure/simplifier.ML	Thu Jun 02 15:52:45 2016 +0200
     3.2 +++ b/src/Pure/simplifier.ML	Thu Jun 02 16:23:10 2016 +0200
     3.3 @@ -45,6 +45,7 @@
     3.4    val prems_of: Proof.context -> thm list
     3.5    val add_simp: thm -> Proof.context -> Proof.context
     3.6    val del_simp: thm -> Proof.context -> Proof.context
     3.7 +  val init_simpset: thm list -> Proof.context -> Proof.context
     3.8    val add_eqcong: thm -> Proof.context -> Proof.context
     3.9    val del_eqcong: thm -> Proof.context -> Proof.context
    3.10    val add_cong: thm -> Proof.context -> Proof.context