# HG changeset patch
# User traytel
# Date 1348999487 -7200
# Node ID 5eb0b0d389eac1a621f8967ce03708e755245902
# Parent  869c7a2e2945d0590c586d84d4f2e97871baa6f1
got rid of subst_tac alias

diff -r 869c7a2e2945 -r 5eb0b0d389ea src/HOL/BNF/Tools/bnf_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Sun Sep 30 12:04:13 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Sun Sep 30 12:04:47 2012 +0200
@@ -13,7 +13,6 @@
   val prefer_tac: int -> tactic
   val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
   val fo_rtac: thm -> Proof.context -> int -> tactic
-  val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic
   val unfold_thms_tac: Proof.context -> thm list -> tactic
   val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
 
@@ -59,9 +58,6 @@
 
 fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
 
-(*unlike "unfold_thms_tac", these succeed when the RHS contains schematic variables not in the LHS*)
-fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];
-
 
 (* Theorems for open typedefs with UNIV as representing set *)