# HG changeset patch
# User wenzelm
# Date 965422571 -7200
# Node ID de95b5125580b27d44067b405f3a3d2b0b2a890c
# Parent  e20323caff4793688e3e3a71a8e5d0b972dd8e18
removed stac (now exported by HypsubstFun);

diff -r e20323caff47 -r de95b5125580 src/FOL/IFOL_lemmas.ML
--- a/src/FOL/IFOL_lemmas.ML	Fri Aug 04 22:55:08 2000 +0200
+++ b/src/FOL/IFOL_lemmas.ML	Fri Aug 04 22:56:11 2000 +0200
@@ -290,17 +290,9 @@
 by (rtac refl 1);
 qed "meta_eq_to_obj_eq";
 
-
-(*Substitution: rule and tactic*)
+(*substitution*)
 bind_thm ("ssubst", sym RS subst);
 
-(*Apply an equality or definition ONCE.
-  Fails unless the substitution has an effect*)
-fun stac th = 
-  let val th' = th RS meta_eq_to_obj_eq handle THM _ => th
-  in  CHANGED_GOAL (rtac (th' RS ssubst))
-  end;
-
 (*A special case of ex1E that would otherwise need quantifier expansion*)
 val prems = Goal
     "[| EX! x. P(x);  P(a);  P(b) |] ==> a=b";
diff -r e20323caff47 -r de95b5125580 src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Fri Aug 04 22:55:08 2000 +0200
+++ b/src/HOL/HOL_lemmas.ML	Fri Aug 04 22:56:11 2000 +0200
@@ -488,13 +488,6 @@
 
 (** Standard abbreviations **)
 
-(*Apply an equality or definition ONCE.
-  Fails unless the substitution has an effect*)
-fun stac th = 
-  let val th' = th RS def_imp_eq handle THM _ => th
-  in  CHANGED_GOAL (rtac (th' RS ssubst))
-  end;
-
 (* combination of (spec RS spec RS ...(j times) ... spec RS mp *) 
 local
   fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t