src/HOL/HOL.ML

--- a/src/HOL/HOL.ML	Sat Jul 10 21:46:15 1999 +0200
+++ b/src/HOL/HOL.ML	Sat Jul 10 21:48:27 1999 +0200
@@ -372,7 +372,7 @@
 (*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 _ => th
+  let val th' = th RS def_imp_eq handle THM _ => th
   in  CHANGED_GOAL (rtac (th' RS ssubst))
   end;