src/Pure/Syntax/mixfix.ML
changeset 6419 702527a8b2a1
parent 6027 9dd06eeda95c
child 6759 8ce58492bf50
equal deleted inserted replaced
6418:87aa3e5190e0 6419:702527a8b2a1
   109 
   109 
   110     fun mfix_of decl =
   110     fun mfix_of decl =
   111       let val t = name_of decl in
   111       let val t = name_of decl in
   112         (case decl of
   112         (case decl of
   113           (_, _, NoSyn) => None
   113           (_, _, NoSyn) => None
   114         | (_, 2, InfixlName (sy, p)) => Some (mk_infix t sy p (p + 1) p)
   114         | (_, 2, InfixlName (sy, p)) => Some (mk_infix sy t p (p + 1) p)
   115         | (_, 2, InfixrName (sy, p)) => Some (mk_infix t sy (p + 1) p p)
   115         | (_, 2, InfixrName (sy, p)) => Some (mk_infix sy t (p + 1) p p)
   116         | (sy, 2, Infixl p) => Some (mk_infix t sy p (p + 1) p)
   116         | (sy, 2, Infixl p) => Some (mk_infix sy t p (p + 1) p)
   117         | (sy, 2, Infixr p) => Some (mk_infix t sy (p + 1) p p)
   117         | (sy, 2, Infixr p) => Some (mk_infix sy t (p + 1) p p)
   118         | _ => error ("Bad mixfix declaration for type " ^ quote t))
   118         | _ => error ("Bad mixfix declaration for type " ^ quote t))
   119       end;
   119       end;
   120 
   120 
   121     val mfix = mapfilter mfix_of type_decls;
   121     val mfix = mapfilter mfix_of type_decls;
   122     val xconsts = map name_of type_decls;
   122     val xconsts = map name_of type_decls;