# HG changeset patch
# User wenzelm
# Date 1329238289 -3600
# Node ID 9b3f6767d1751b8067851bb11b412f73ef96c15d
# Parent  7524f3ac737c612bb4a0ce362ad4acb7e9210114
eliminated unused rewrite_goal_rule;

diff -r 7524f3ac737c -r 9b3f6767d175 src/Pure/raw_simplifier.ML
--- 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 **)