Removed superfluous type constraint
authornipkow
Mon, 13 Mar 1995 09:42:50 +0100
changeset 950 323f8ca4587a
parent 949 83c588d6fee9
child 951 682139612060
Removed superfluous type constraint
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)*)