--- 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
--- 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 =