--- a/WF.ML	Wed Mar 08 17:22:28 1995 +0100
+++ b/WF.ML	Mon Mar 13 09:41:20 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)*)