# HG changeset patch
# User wenzelm
# Date 777663065 -7200
# Node ID 2fa5ef27bd0aa6dd04a2fb352c765d706984d245
# Parent  13c30ac40f8fb36b823ba1f406dd0000acba46b2
removed constant _constrain from Pure sig;

diff -r 13c30ac40f8f -r 2fa5ef27bd0a src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Aug 22 11:27:23 1994 +0200
+++ b/src/Pure/sign.ML	Tue Aug 23 19:31:05 1994 +0200
@@ -6,7 +6,6 @@
 
 TODO:
   clean
-  pure sign: elim Syntax.constrainC
 *)
 
 signature SIGN =
@@ -523,8 +522,7 @@
     ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
     ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
     ("all", "('a => prop) => prop", Binder ("!!", 0)),
-    ("TYPE", "'a itself", NoSyn)(*,(* FIXME *)
-    (Syntax.constrainC, "'a::{} => 'a", NoSyn)*)]
+    ("TYPE", "'a itself", NoSyn)]
   |> add_name "Pure";