src/Pure/sign.ML
changeset 573 2fa5ef27bd0a
parent 562 e9572d03b724
child 583 550292083e66
     1.1 --- a/src/Pure/sign.ML	Mon Aug 22 11:27:23 1994 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Aug 23 19:31:05 1994 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  TODO:
     1.6    clean
     1.7 -  pure sign: elim Syntax.constrainC
     1.8  *)
     1.9  
    1.10  signature SIGN =
    1.11 @@ -523,8 +522,7 @@
    1.12      ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
    1.13      ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
    1.14      ("all", "('a => prop) => prop", Binder ("!!", 0)),
    1.15 -    ("TYPE", "'a itself", NoSyn)(*,(* FIXME *)
    1.16 -    (Syntax.constrainC, "'a::{} => 'a", NoSyn)*)]
    1.17 +    ("TYPE", "'a itself", NoSyn)]
    1.18    |> add_name "Pure";
    1.19  
    1.20