# HG changeset patch
# User wenzelm
# Date 973879950 -3600
# Node ID 2dfa192367680d414809989d73d6de0f3c234ef0
# Parent  0a68dc9edba597f3bdae8f4f4405498003840514
added rewrite_goal_tac;

diff -r 0a68dc9edba5 -r 2dfa19236768 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Nov 10 19:11:51 2000 +0100
+++ b/src/Pure/tactic.ML	Fri Nov 10 19:12:30 2000 +0100
@@ -81,6 +81,7 @@
   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_goal_tac  : thm list -> int -> tactic
   val rewrite_goals_rule: thm list -> thm -> thm
   val rewrite_rule	: thm list -> thm -> thm
   val rewrite_goals_tac	: thm list -> tactic
@@ -492,12 +493,14 @@
         (PRIMITIVE
 	   (rewrite_goal_rule mode (result1 prover_tac) mss 1));
 
+fun rewrite_goal_tac rews =
+  asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
+
 (*Rewrite throughout proof state. *)
 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
 
 (*Rewrite subgoals only, not main goal. *)
 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
-
 fun rewtac def = rewrite_goals_tac [def];