1.1 --- a/src/HOL/W0/I.ML	Thu Aug 20 16:18:39 1998 +0200
     1.2 +++ b/src/HOL/W0/I.ML	Thu Aug 20 16:20:17 1998 +0200
     1.3 @@ -8,8 +8,7 @@
     1.4  
     1.5  open I;
     1.6  
     1.7 -Goal
     1.8 -  "! a m s s' t n.  \
     1.9 +Goal "! a m s s' t n.  \
    1.10  \    (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) -->   \
    1.11  \    ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )";
    1.12  by (induct_tac "e" 1);
    1.13 @@ -123,8 +122,7 @@
    1.14  (***
    1.15  We actually want the corollary
    1.16  
    1.17 -Goal
    1.18 -  "I e [] m id_subst = Ok(s,t,n) --> W e [] m = Ok(s, $s t, n)";
    1.19 +Goal "I e [] m id_subst = Ok(s,t,n) --> W e [] m = Ok(s, $s t, n)";
    1.20  by (cut_facts_tac [(read_instantiate[("x","id_subst")]
    1.21   (read_instantiate[("x","[]")](thm RS spec)
    1.22    RS spec RS spec))] 1);