diff -r 83c588d6fee9 -r 323f8ca4587a src/HOL/WF.ML
--- a/src/HOL/WF.ML	Mon Mar 13 09:38:10 1995 +0100
+++ b/src/HOL/WF.ML	Mon Mar 13 09:42:50 1995 +0100
@@ -8,8 +8,7 @@
 
 open WF;
 
-val H_cong = read_instantiate [("f","H::[?'a, ?'a=>?'b]=>?'b")]
-               (standard(refl RS cong RS cong));
+val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong));
 val H_cong1 = refl RS H_cong;
 
 (*Restriction to domain A.  If r is well-founded over A then wf(r)*)