src/Pure/sign.ML
changeset 410 c8171ee32744
parent 402 16a8fe4f2250
child 418 ab09293bccc7
     1.1 --- a/src/Pure/sign.ML	Wed Jun 01 13:18:35 1994 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Jun 01 15:42:25 1994 +0200
     1.3 @@ -547,27 +547,27 @@
     1.4  
     1.5  val pure =
     1.6    make_sign (Syntax.type_syn, tsig0, Symtab.null) [] "#"
     1.7 -  also add_types
     1.8 +  |> add_types
     1.9     (("fun", 2, NoSyn) ::
    1.10      ("prop", 0, NoSyn) ::
    1.11      ("itself", 1, NoSyn) ::
    1.12      Syntax.Mixfix.pure_types)
    1.13 -  also add_classes [([], logicC, [])]
    1.14 -  also add_defsort logicS
    1.15 -  also add_arities
    1.16 +  |> add_classes [([], logicC, [])]
    1.17 +  |> add_defsort logicS
    1.18 +  |> add_arities
    1.19     [("fun", [logicS, logicS], logicS),
    1.20      ("prop", [], logicS),
    1.21      ("itself", [logicS], logicS)]
    1.22 -  also add_syntax Syntax.Mixfix.pure_syntax
    1.23 -  also add_trfuns Syntax.pure_trfuns
    1.24 -  also add_consts
    1.25 +  |> add_syntax Syntax.Mixfix.pure_syntax
    1.26 +  |> add_trfuns Syntax.pure_trfuns
    1.27 +  |> add_consts
    1.28     [("==", "['a::{}, 'a] => prop", Mixfix ("(_ ==/ _)", [3, 2], 2)),
    1.29      ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
    1.30      ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
    1.31      ("all", "('a => prop) => prop", Binder ("!!", 0)),
    1.32      ("TYPE", "'a itself", NoSyn),
    1.33      (Syntax.constrainC, "'a::{} => 'a", NoSyn)]
    1.34 -  also add_name "Pure";
    1.35 +  |> add_name "Pure";
    1.36  
    1.37  
    1.38  end;