src/Pure/raw_simplifier.ML

--- a/src/Pure/raw_simplifier.ML	Fri Dec 13 23:53:02 2013 +0100
+++ b/src/Pure/raw_simplifier.ML	Sat Dec 14 17:28:05 2013 +0100
@@ -57,13 +57,13 @@
   val setSolver: Proof.context * solver -> Proof.context
   val addSolver: Proof.context * solver -> Proof.context
 
-  val rewrite_rule: thm list -> thm -> thm
-  val rewrite_goals_rule: thm list -> thm -> thm
-  val rewrite_goals_tac: thm list -> tactic
-  val rewrite_goal_tac: thm list -> int -> tactic
-  val prune_params_tac: tactic
-  val fold_rule: thm list -> thm -> thm
-  val fold_goals_tac: thm list -> tactic
+  val rewrite_rule: Proof.context -> thm list -> thm -> thm
+  val rewrite_goals_rule: Proof.context -> thm list -> thm -> thm
+  val rewrite_goals_tac: Proof.context -> thm list -> tactic
+  val rewrite_goal_tac: Proof.context -> thm list -> int -> tactic
+  val prune_params_tac: Proof.context -> tactic
+  val fold_rule: Proof.context -> thm list -> thm -> thm
+  val fold_goals_tac: Proof.context -> thm list -> tactic
   val norm_hhf: thm -> thm
   val norm_hhf_protect: thm -> thm
 end;
@@ -126,7 +126,7 @@
     (Proof.context -> thm -> thm option) -> Proof.context -> thm -> thm
   val generic_rewrite_goal_tac: bool * bool * bool ->
     (Proof.context -> tactic) -> Proof.context -> int -> tactic
-  val rewrite: bool -> thm list -> conv
+  val rewrite: Proof.context -> bool -> thm list -> conv
 end;
 
 structure Raw_Simplifier: RAW_SIMPLIFIER =
@@ -1366,12 +1366,12 @@
 val simple_prover =
   SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));
 
-fun rewrite _ [] ct = Thm.reflexive ct
-  | rewrite full thms ct =
+fun rewrite _ _ [] = Thm.reflexive
+  | rewrite ctxt full thms =
       rewrite_cterm (full, false, false) simple_prover
-        (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
+        (empty_simpset ctxt addsimps thms);
 
-val rewrite_rule = Conv.fconv_rule o rewrite true;
+fun rewrite_rule ctxt = Conv.fconv_rule o rewrite ctxt true;
 
 (*simple term rewriting -- no proof*)
 fun rewrite_term thy rules procs =
@@ -1380,15 +1380,15 @@
 fun rewrite_thm mode prover ctxt = Conv.fconv_rule (rewrite_cterm mode prover ctxt);
 
 (*Rewrite the subgoals of a proof state (represented by a theorem)*)
-fun rewrite_goals_rule thms th =
+fun rewrite_goals_rule ctxt thms th =
   Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
-    (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
+    (empty_simpset ctxt addsimps thms))) th;
 
 
 (** meta-rewriting tactics **)
 
 (*Rewrite all subgoals*)
-fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
+fun rewrite_goals_tac ctxt defs = PRIMITIVE (rewrite_goals_rule ctxt defs);
 
 (*Rewrite one subgoal*)
 fun generic_rewrite_goal_tac mode prover_tac ctxt i thm =
@@ -1396,12 +1396,12 @@
     Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ctxt) i thm)
   else Seq.empty;
 
-fun rewrite_goal_tac rews i st =
+fun rewrite_goal_tac ctxt rews =
   generic_rewrite_goal_tac (true, false, false) (K no_tac)
-    (global_context (Thm.theory_of_thm st) empty_ss addsimps rews) i st;
+    (empty_simpset ctxt addsimps rews);
 
 (*Prunes all redundant parameters from the proof state by rewriting.*)
-val prune_params_tac = rewrite_goals_tac [Drule.triv_forall_equality];
+fun prune_params_tac ctxt = rewrite_goals_tac ctxt [Drule.triv_forall_equality];
 
 
 (* for folding definitions, handling critical pairs *)
@@ -1422,8 +1422,8 @@
 
 val rev_defs = sort_lhs_depths o map Thm.symmetric;
 
-fun fold_rule defs = fold rewrite_rule (rev_defs defs);
-fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
+fun fold_rule ctxt defs = fold (rewrite_rule ctxt) (rev_defs defs);
+fun fold_goals_tac ctxt defs = EVERY (map (rewrite_goals_tac ctxt) (rev_defs defs));
 
 
 (* HHF normal form: !! before ==>, outermost !! generalized *)