src/Pure/sign.ML
changeset 1178 b28c6ecc3e6d
parent 1159 998a5c3451bf
child 1180 9b2efb601898
     1.1 --- a/src/Pure/sign.ML	Mon Jul 03 13:37:29 1995 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon Jul 03 15:39:53 1995 +0200
     1.3 @@ -308,7 +308,7 @@
     1.4       | Ambigs(us) =>
     1.5           (warn();
     1.6            let val old_show_brackets = !show_brackets
     1.7 -              val _ = show_brackets := true;
     1.8 +              val dummy = show_brackets := true;
     1.9                val errs = cat_lines(map show_term us)
    1.10            in show_brackets := old_show_brackets;
    1.11               error("Error: More than one term is type correct:\n" ^ errs)
    1.12 @@ -553,12 +553,16 @@
    1.13  
    1.14  val cpure = proto_pure
    1.15    |> add_syntax
    1.16 -   [("_applC",     "[('b => 'a), 'c] => logic",     Mixfix ("_/ _",
    1.17 -                                                    [max_pri-1, max_pri],
    1.18 -                                                    max_pri-1)),
    1.19 -    ("_applC",     "[('b => 'a), 'c] => aprop",     Mixfix ("_/ _",
    1.20 -                                                    [max_pri-1, max_pri],
    1.21 -                                                    max_pri-1))]
    1.22 +   [("",           "'a => cargs",                   Delimfix "_"),
    1.23 +    ("_cargs",     "['a, cargs] => cargs",          Mixfix ("_/ _",
    1.24 +                                                     [max_pri, max_pri],
    1.25 +                                                     max_pri)),
    1.26 +    ("_applC",     "[('b => 'a), cargs] => logic",  Mixfix ("(1_/ _)",
    1.27 +                                                     [max_pri, max_pri],
    1.28 +                                                     max_pri-1)),
    1.29 +    ("_applC",     "[('b => 'a), cargs] => aprop",  Mixfix ("(1_/ _)",
    1.30 +                                                     [max_pri, max_pri],
    1.31 +                                                     max_pri-1))]
    1.32    |> add_name "CPure";
    1.33  
    1.34  end;