src/HOL/WF.ML
changeset 950 323f8ca4587a
parent 923 ff1574a81019
child 972 e61b058d58d2
     1.1 --- a/src/HOL/WF.ML	Mon Mar 13 09:38:10 1995 +0100
     1.2 +++ b/src/HOL/WF.ML	Mon Mar 13 09:42:50 1995 +0100
     1.3 @@ -8,8 +8,7 @@
     1.4  
     1.5  open WF;
     1.6  
     1.7 -val H_cong = read_instantiate [("f","H::[?'a, ?'a=>?'b]=>?'b")]
     1.8 -               (standard(refl RS cong RS cong));
     1.9 +val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong));
    1.10  val H_cong1 = refl RS H_cong;
    1.11  
    1.12  (*Restriction to domain A.  If r is well-founded over A then wf(r)*)