# HG changeset patch
# User wenzelm
# Date 1183475835 -7200
# Node ID 77886dfbfa33b292cda87a5fde54e64ec00a560d
# Parent  df5440e241a14d37a3b92d4ef362a803e6fa2fb6
CONVERSION tactical;
MetaSimplifier.rewrite_goal_tac;

diff -r df5440e241a1 -r 77886dfbfa33 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Tue Jul 03 17:17:13 2007 +0200
+++ b/src/Pure/Isar/object_logic.ML	Tue Jul 03 17:17:15 2007 +0200
@@ -141,10 +141,8 @@
 
 (* atomize *)
 
-fun rewrite_prems_tac rews i = PRIMITIVE (Conv.fconv_rule
-  (Conv.goals_conv (Library.equal i)
-    (Conv.forall_conv ~1
-      (Conv.goals_conv (K true) (MetaSimplifier.rewrite true rews)))));
+fun rewrite_prems_tac rews =
+  CONVERSION (Conv.forall_conv ~1 (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true rews))));
 
 fun atomize_term thy =
   drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
@@ -158,7 +156,7 @@
   else all_tac st;
 
 fun full_atomize_tac i st =
-  Goal.rewrite_goal_tac (get_atomize (Thm.theory_of_thm st)) i st;
+  MetaSimplifier.rewrite_goal_tac (get_atomize (Thm.theory_of_thm st)) i st;
 
 fun atomize_goal i st =
   (case Seq.pull (atomize_tac i st) of NONE => st | SOME (st', _) => st');
@@ -167,7 +165,7 @@
 (* rulify *)
 
 fun rulify_term thy = MetaSimplifier.rewrite_term thy (get_rulify thy) [];
-fun rulify_tac i st = Goal.rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
+fun rulify_tac i st = MetaSimplifier.rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
 
 fun gen_rulify full thm =
   MetaSimplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm