improved rewrite_thm / rewrite_goals to handle conditional eqns;

--- a/src/Pure/drule.ML	Thu Jul 24 15:25:29 1997 +0200
+++ b/src/Pure/drule.ML	Fri Jul 25 11:47:09 1997 +0200
@@ -48,8 +48,8 @@
   val revcut_rl		: thm
   val rewrite_goal_rule	: bool * bool -> (meta_simpset -> thm -> thm option)
         -> meta_simpset -> int -> thm -> thm
-  val rewrite_goals_rule: thm list -> thm -> thm
-  val rewrite_rule	: thm list -> thm -> thm
+  val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
+  val rewrite_rule_aux	: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
   val rewrite_thm	: bool * bool -> (meta_simpset -> thm -> thm option)
 	-> meta_simpset -> thm -> thm
   val RS		: thm * thm -> thm
@@ -548,19 +548,17 @@
 fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
 
 (*Rewrite a theorem*)
-fun rewrite_rule []   th = th
-  | rewrite_rule thms th =
-	fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms)) th;
+fun rewrite_rule_aux _ []   th = th
+  | rewrite_rule_aux prover thms th =
+      fconv_rule (rew_conv (true,false) prover (Thm.mss_of thms)) th;
 
 fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
 
 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
-fun rewrite_goals_rule []   th = th
-  | rewrite_goals_rule thms th =
-	fconv_rule (goals_conv (K true) 
-		    (rew_conv (true,false) (K(K None))
-		     (Thm.mss_of thms))) 
-	           th;
+fun rewrite_goals_rule_aux _ []   th = th
+  | rewrite_goals_rule_aux prover thms th =
+      fconv_rule (goals_conv (K true) (rew_conv (true, true) prover
+        (Thm.mss_of thms))) th;
 
 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
 fun rewrite_goal_rule mode prover mss i thm =

--- a/src/Pure/tactic.ML	Thu Jul 24 15:25:29 1997 +0200
+++ b/src/Pure/tactic.ML	Fri Jul 25 11:47:09 1997 +0200
@@ -1,4 +1,4 @@
-(*  Title: 	tactic
+(*  Title: 	Pure/tactic.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
@@ -72,6 +72,8 @@
   val resolve_from_net_tac	: (int*thm) Net.net -> int -> tactic
   val resolve_tac	: thm list -> int -> tactic
   val res_inst_tac	: (string*string)list -> thm -> int -> tactic   
+  val rewrite_goals_rule: thm list -> thm -> thm
+  val rewrite_rule	: thm list -> thm -> thm
   val rewrite_goals_tac	: thm list -> tactic
   val rewrite_tac	: thm list -> tactic
   val rewtac		: thm -> tactic
@@ -473,6 +475,13 @@
 fun result1 tacf mss thm =
   apsome fst (Sequence.pull (tacf mss thm));
 
+val simple_prover =
+  result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss)));
+
+val rewrite_rule = Drule.rewrite_rule_aux simple_prover;
+val rewrite_goals_rule = Drule.rewrite_goals_rule_aux simple_prover;
+
+
 (*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
 fun asm_rewrite_goal_tac mode prover_tac mss =
       SELECT_GOAL