src/Pure/Syntax/mixfix.ML
changeset 2677 d73a46247a4a
parent 2675 e2908f8edc8d
child 2696 a41b9ee247ec
equal deleted inserted replaced
2676:585cd2311a98 2677:d73a46247a4a
   154 (** Pure syntax **)
   154 (** Pure syntax **)
   155 
   155 
   156 val pure_types =
   156 val pure_types =
   157   map (fn t => (t, 0, NoSyn))
   157   map (fn t => (t, 0, NoSyn))
   158     (terminals @ [logic, "type", "types", "sort", "classes", args, cargs,
   158     (terminals @ [logic, "type", "types", "sort", "classes", args, cargs,
   159       "pttrn", "idt", "idts", "aprop", "asms", any, sprop]);
   159       "pttrn", "idt", "idts", "aprop", "asms", any, sprop, "dummy"]);
   160 
   160 
   161 val pure_syntax =
   161 val pure_syntax =
   162  [("_lambda",   "[idts, 'a] => logic",            Mixfix ("(3%_./ _)", [], 0)),
   162  [("_lambda",   "[idts, 'a] => logic",            Mixfix ("(3%_./ _)", [], 0)),
   163   ("_abs",      "'a",                             NoSyn),
   163   ("_abs",      "'a",                             NoSyn),
   164   ("",          "'a => " ^ args,                  Delimfix "_"),
   164   ("",          "'a => " ^ args,                  Delimfix "_"),