src/Pure/sign.ML
changeset 865 b38c67991122
parent 763 d5a626aacdd3
child 879 27675591cc50
     1.1 --- a/src/Pure/sign.ML	Wed Jan 18 10:17:55 1995 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Jan 18 11:36:04 1995 +0100
     1.3 @@ -428,9 +428,7 @@
     1.4    (Syntax.extend_trfuns syn trfuns, tsig, ctab);
     1.5  
     1.6  fun ext_trrules (syn, tsig, ctab) xrules =
     1.7 -  (Syntax.extend_trrules syn
     1.8 -  (infer_types (Sg {tsig = tsig, const_tab = ctab, syn = syn, 
     1.9 -                   stamps = [ref "#"]}) (K None) (K None)) xrules, tsig, ctab);
    1.10 +  (Syntax.extend_trrules syn xrules, tsig, ctab);
    1.11  
    1.12  
    1.13  (* build signature *)
    1.14 @@ -530,7 +528,7 @@
    1.15     [("==", "['a::{}, 'a] => prop", Mixfix ("(_ ==/ _)", [3, 2], 2)),
    1.16      ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
    1.17      ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
    1.18 -    ("all", "('a => prop) => prop", Binder ("!!", 0)),
    1.19 +    ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
    1.20      ("TYPE", "'a itself", NoSyn)]
    1.21    |> add_name "Pure";
    1.22