--- 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