--- a/src/HOL/BNF/Tools/bnf_tactics.ML Thu Sep 27 18:39:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Thu Sep 27 18:58:15 2012 +0200
@@ -14,7 +14,6 @@
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 substs_tac: Proof.context -> 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
@@ -62,7 +61,6 @@
(*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];
-fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt NONE;
(* Theorems for open typedefs with UNIV as representing set *)