# HG changeset patch
# User wenzelm
# Date 1329236795 -3600
# Node ID 68cf3d3550b5d72ab7e0b2e83e81d39cce365c36
# Parent  73823dbbecc40d634858df124a19a142b8825cf7
eliminated obsolete aliases;

diff -r 73823dbbecc4 -r 68cf3d3550b5 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Tue Feb 14 17:11:33 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Tue Feb 14 17:26:35 2012 +0100
@@ -308,7 +308,7 @@
     val nargs = length (binder_types T)
     val pred_case_rule = the_elim_of ctxt pred
   in
-    REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
+    REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all}))
     THEN print_tac options "before applying elim rule"
     THEN etac (predfun_elim_of ctxt pred mode) 1
     THEN etac pred_case_rule 1
@@ -385,7 +385,7 @@
           val ho_args = ho_args_of mode args
         in
           etac @{thm bindE} 1
-          THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
+          THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})))
           THEN print_tac options "prove_expr2-before"
           THEN etac (predfun_elim_of ctxt name mode) 1
           THEN print_tac options "prove_expr2"
@@ -496,7 +496,7 @@
       THEN (prove_clause2 options ctxt pred mode clause i)
   in
     (DETERM (TRY (rtac @{thm unit.induct} 1)))
-     THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
+     THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})))
      THEN (rtac (predfun_intro_of ctxt pred mode) 1)
      THEN (REPEAT_DETERM (rtac @{thm refl} 2))
      THEN (if null moded_clauses then
diff -r 73823dbbecc4 -r 68cf3d3550b5 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Feb 14 17:11:33 2012 +0100
+++ b/src/Pure/raw_simplifier.ML	Tue Feb 14 17:26:35 2012 +0100
@@ -55,7 +55,6 @@
   val rewrite_goals_rule: thm list -> thm -> thm
   val rewrite_goals_tac: thm list -> tactic
   val rewrite_goal_tac: thm list -> int -> tactic
-  val rewtac: thm -> tactic
   val prune_params_tac: tactic
   val fold_rule: thm list -> thm -> thm
   val fold_goals_tac: thm list -> tactic
@@ -1305,7 +1304,6 @@
 
 (*Rewrite all subgoals*)
 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
-fun rewtac def = rewrite_goals_tac [def];
 
 (*Rewrite one subgoal*)
 fun asm_rewrite_goal_tac mode prover_tac ss i thm =