--- a/src/Pure/raw_simplifier.ML Tue Feb 14 17:49:47 2012 +0100
+++ b/src/Pure/raw_simplifier.ML Tue Feb 14 17:51:29 2012 +0100
@@ -123,8 +123,6 @@
val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
val rewrite_thm: bool * bool * bool ->
(simpset -> thm -> thm option) -> simpset -> thm -> thm
- val rewrite_goal_rule: bool * bool * bool ->
- (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
val asm_rewrite_goal_tac: bool * bool * bool ->
(simpset -> tactic) -> simpset -> int -> tactic
val rewrite: bool -> thm list -> conv
@@ -1293,12 +1291,6 @@
Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
(global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
-(*Rewrite the subgoal of a proof state (represented by a theorem)*)
-fun rewrite_goal_rule mode prover ss i thm =
- if 0 < i andalso i <= Thm.nprems_of thm
- then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
- else raise THM ("rewrite_goal_rule", i, [thm]);
-
(** meta-rewriting tactics **)