--- 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