src/HOL/HOL.ML
changeset 1672 2c109cd2fdd0
parent 1668 8ead1fe65aad
child 1725 8b7414384396
     1.1 --- a/src/HOL/HOL.ML	Tue Apr 23 16:44:22 1996 +0200
     1.2 +++ b/src/HOL/HOL.ML	Tue Apr 23 16:58:21 1996 +0200
     1.3 @@ -305,7 +305,7 @@
     1.4  
     1.5  (** Standard abbreviations **)
     1.6  
     1.7 -fun stac th = rtac(th RS ssubst);
     1.8 +fun stac th = CHANGED o rtac (th RS ssubst);
     1.9  fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
    1.10  
    1.11  (** strip proved goal while preserving !-bound var names **)