# HG changeset patch
# User wenzelm
# Date 973879981 -3600
# Node ID 59265527d9eb29bc48805865086cd809d57a98a8
# Parent  2dfa192367680d414809989d73d6de0f3c234ef0
rewrite_goal_tac moved to tactic.ML;

diff -r 2dfa19236768 -r 59265527d9eb src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Nov 10 19:12:30 2000 +0100
+++ b/src/Pure/Isar/method.ML	Fri Nov 10 19:13:01 2000 +0100
@@ -39,7 +39,6 @@
   val insert_facts: Proof.method
   val unfold: thm list -> Proof.method
   val fold: thm list -> Proof.method
-  val rewrite_goal_tac: thm list -> int -> tactic
   val atomize_tac: thm list -> int -> tactic
   val atomize_goal: thm list -> int -> thm -> thm
   val multi_resolve: thm list -> thm -> thm Seq.seq
@@ -278,9 +277,6 @@
 
 (* atomize meta-connectives *)
 
-fun rewrite_goal_tac rews =
-  Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
-
 fun atomize_tac rews =
   let val rew_tac = rewrite_goal_tac rews in
     fn i => fn thm =>