diff -r a766de752996 -r cfa87aef9ccd src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Sat Jul 10 21:43:27 1999 +0200
+++ b/src/FOL/IFOL.ML	Sat Jul 10 21:44:26 1999 +0200
@@ -248,7 +248,7 @@
 (*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 _ => th
+  let val th' = th RS meta_eq_to_obj_eq handle THM _ => th
   in  CHANGED_GOAL (rtac (th' RS ssubst))
   end;