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