# HG changeset patch
# User nipkow
# Date 795084170 -3600
# Node ID 323f8ca4587a90c4812041027ad6ccde33c508de
# Parent  83c588d6fee965843fdf9c4c2f6dacf107e971ed
Removed superfluous type constraint

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)*)