src/HOL/HOL.ML
changeset 6968 7f2977e96a5c
parent 6513 e0a9459e99fc
child 7030 53934985426a
     1.1 --- a/src/HOL/HOL.ML	Sat Jul 10 21:46:15 1999 +0200
     1.2 +++ b/src/HOL/HOL.ML	Sat Jul 10 21:48:27 1999 +0200
     1.3 @@ -372,7 +372,7 @@
     1.4  (*Apply an equality or definition ONCE.
     1.5    Fails unless the substitution has an effect*)
     1.6  fun stac th = 
     1.7 -  let val th' = th RS def_imp_eq handle _ => th
     1.8 +  let val th' = th RS def_imp_eq handle THM _ => th
     1.9    in  CHANGED_GOAL (rtac (th' RS ssubst))
    1.10    end;
    1.11