# HG changeset patch
# User wenzelm
# Date 1003089946 -7200
# Node ID 48bc55f4377461fb6b20daf44dce90900bcc593e
# Parent  7380c9d45626df8349acec33d91e7f5a572a6bc3
unified rewrite/rewrite_cterm/simplify interface;

diff -r 7380c9d45626 -r 48bc55f43774 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Sun Oct 14 22:05:01 2001 +0200
+++ b/src/Pure/tactic.ML	Sun Oct 14 22:05:46 2001 +0200
@@ -83,8 +83,9 @@
   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 full_rewrite      : thm list -> cterm -> thm
-  val full_rewrite_cterm : thm list -> cterm -> cterm
+  val rewrite           : bool -> thm list -> cterm -> thm
+  val rewrite_cterm     : bool -> thm list -> cterm -> cterm
+  val simplify          : bool -> thm list -> thm -> thm
   val rewrite_goal_tac  : thm list -> int -> tactic
   val rewrite_goals_rule: thm list -> thm -> thm
   val rewrite_rule      : thm list -> thm -> thm
@@ -487,9 +488,10 @@
 val simple_prover =
   result1 (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss)));
 
-val full_rewrite = MetaSimplifier.full_rewrite_aux simple_prover;
-val full_rewrite_cterm = (#2 o Thm.dest_comb o #prop o Thm.crep_thm) oo full_rewrite;
-val rewrite_rule = MetaSimplifier.rewrite_rule_aux simple_prover;
+val rewrite = MetaSimplifier.rewrite_aux simple_prover;
+val rewrite_cterm = (#2 o Thm.dest_comb o #prop o Thm.crep_thm) ooo rewrite;
+val simplify = MetaSimplifier.simplify_aux simple_prover;
+val rewrite_rule = simplify true;
 val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
 
 (*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)