# HG changeset patch
# User wenzelm
# Date 1464877390 -7200
# Node ID 7d43fbbaba2833c1a013d2a9766e5c10efdf4b11
# Parent  06cbfbaf39c5666ec210f96cdba3af3417f0ef6e
avoid warnings on duplicate rules in the given list;

diff -r 06cbfbaf39c5 -r 7d43fbbaba28 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Thu Jun 02 15:52:45 2016 +0200
+++ b/src/Pure/Isar/local_defs.ML	Thu Jun 02 16:23:10 2016 +0200
@@ -196,8 +196,8 @@
 
 fun meta_rewrite_conv ctxt =
   Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
-    (empty_simpset ctxt
-      addsimps (Rules.get (Context.Proof ctxt))
+    (ctxt
+      |> Raw_Simplifier.init_simpset (Rules.get (Context.Proof ctxt))
       |> Raw_Simplifier.add_eqcong Drule.equals_cong);    (*protect meta-level equality*)
 
 val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv;
diff -r 06cbfbaf39c5 -r 7d43fbbaba28 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu Jun 02 15:52:45 2016 +0200
+++ b/src/Pure/raw_simplifier.ML	Thu Jun 02 16:23:10 2016 +0200
@@ -90,6 +90,7 @@
   val prems_of: Proof.context -> thm list
   val add_simp: thm -> Proof.context -> Proof.context
   val del_simp: thm -> Proof.context -> Proof.context
+  val init_simpset: thm list -> Proof.context -> Proof.context
   val add_eqcong: thm -> Proof.context -> Proof.context
   val del_eqcong: thm -> Proof.context -> Proof.context
   val add_cong: thm -> Proof.context -> Proof.context
@@ -589,6 +590,12 @@
 
 end;
 
+fun init_simpset thms ctxt = ctxt
+  |> Context_Position.set_visible false
+  |> empty_simpset
+  |> fold add_simp thms
+  |> Context_Position.restore_visible ctxt;
+
 
 (* congs *)
 
@@ -1314,8 +1321,7 @@
 
 fun rewrite _ _ [] = Thm.reflexive
   | rewrite ctxt full thms =
-      rewrite_cterm (full, false, false) simple_prover
-        (empty_simpset ctxt addsimps thms);
+      rewrite_cterm (full, false, false) simple_prover (init_simpset thms ctxt);
 
 fun rewrite_rule ctxt = Conv.fconv_rule o rewrite ctxt true;
 
@@ -1328,7 +1334,7 @@
 (*Rewrite the subgoals of a proof state (represented by a theorem)*)
 fun rewrite_goals_rule ctxt thms th =
   Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
-    (empty_simpset ctxt addsimps thms))) th;
+    (init_simpset thms ctxt))) th;
 
 
 (** meta-rewriting tactics **)
@@ -1342,9 +1348,8 @@
     Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ctxt) i thm)
   else Seq.empty;
 
-fun rewrite_goal_tac ctxt rews =
-  generic_rewrite_goal_tac (true, false, false) (K no_tac)
-    (empty_simpset ctxt addsimps rews);
+fun rewrite_goal_tac ctxt thms =
+  generic_rewrite_goal_tac (true, false, false) (K no_tac) (init_simpset thms ctxt);
 
 (*Prunes all redundant parameters from the proof state by rewriting.*)
 fun prune_params_tac ctxt = rewrite_goals_tac ctxt [Drule.triv_forall_equality];
@@ -1387,11 +1392,15 @@
   Variable.gen_all ctxt;
 
 val hhf_ss =
-  simpset_of (empty_simpset (Context.the_local_context ()) addsimps Drule.norm_hhf_eqs);
+  Context.the_local_context ()
+  |> init_simpset Drule.norm_hhf_eqs
+  |> simpset_of;
 
 val hhf_protect_ss =
-  simpset_of (empty_simpset (Context.the_local_context ())
-    addsimps Drule.norm_hhf_eqs |> add_eqcong Drule.protect_cong);
+  Context.the_local_context ()
+  |> init_simpset Drule.norm_hhf_eqs
+  |> add_eqcong Drule.protect_cong
+  |> simpset_of;
 
 in
 
diff -r 06cbfbaf39c5 -r 7d43fbbaba28 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Jun 02 15:52:45 2016 +0200
+++ b/src/Pure/simplifier.ML	Thu Jun 02 16:23:10 2016 +0200
@@ -45,6 +45,7 @@
   val prems_of: Proof.context -> thm list
   val add_simp: thm -> Proof.context -> Proof.context
   val del_simp: thm -> Proof.context -> Proof.context
+  val init_simpset: thm list -> Proof.context -> Proof.context
   val add_eqcong: thm -> Proof.context -> Proof.context
   val del_eqcong: thm -> Proof.context -> Proof.context
   val add_cong: thm -> Proof.context -> Proof.context