src/Pure/Syntax/mixfix.ML
changeset 42297 140f283266b7
parent 42293 6cca0343ea48
child 42298 d622145603ee
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 21:03:20 2011 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 21:11:29 2011 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4  
     1.5      fun mfix_of (_, _, NoSyn) = NONE
     1.6        | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syntax_Ext.Mfix (sy, ty, t, ps, p))
     1.7 -      | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], Syntax_Ext.max_pri))
     1.8 +      | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], 1000))
     1.9        | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
    1.10        | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
    1.11        | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
    1.12 @@ -122,7 +122,7 @@
    1.13  fun syn_ext_consts is_logtype const_decls =
    1.14    let
    1.15      fun mk_infix sy ty c p1 p2 p3 =
    1.16 -      [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], Syntax_Ext.max_pri),
    1.17 +      [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], 1000),
    1.18         Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
    1.19  
    1.20      fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
    1.21 @@ -131,7 +131,7 @@
    1.22  
    1.23      fun mfix_of (_, _, NoSyn) = []
    1.24        | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syntax_Ext.Mfix (sy, ty, c, ps, p)]
    1.25 -      | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], Syntax_Ext.max_pri)]
    1.26 +      | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], 1000)]
    1.27        | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
    1.28        | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
    1.29        | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p