src/Pure/Syntax/mixfix.ML
changeset 62760 aabcc727aa2d
parent 62759 d16b2ec535ba
child 62761 5c672b22dcc2
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Mar 30 14:52:23 2016 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Mar 30 14:59:12 2016 +0200
     1.3 @@ -22,7 +22,6 @@
     1.4    include BASIC_MIXFIX
     1.5    val is_empty: mixfix -> bool
     1.6    val equal: mixfix * mixfix -> bool
     1.7 -  val set_range: Position.range -> mixfix -> mixfix
     1.8    val range_of: mixfix -> Position.range
     1.9    val pos_of: mixfix -> Position.T
    1.10    val reset_pos: mixfix -> mixfix
    1.11 @@ -65,17 +64,6 @@
    1.12    | equal (Structure _, Structure _) = true
    1.13    | equal _ = false;
    1.14  
    1.15 -fun set_range range mx =
    1.16 -  (case mx of
    1.17 -    NoSyn => NoSyn
    1.18 -  | Mixfix (sy, ps, p, _) => Mixfix (sy, ps, p, range)
    1.19 -  | Delimfix (sy, _) => Delimfix (sy, range)
    1.20 -  | Infix (sy, p, _) => Infix (sy, p, range)
    1.21 -  | Infixl (sy, p, _) => Infixl (sy, p, range)
    1.22 -  | Infixr (sy, p, _) => Infixr (sy, p, range)
    1.23 -  | Binder (sy, p, q, _) => Binder (sy, p, q, range)
    1.24 -  | Structure _ => Structure range);
    1.25 -
    1.26  fun range_of NoSyn = Position.no_range
    1.27    | range_of (Mixfix (_, _, _, range)) = range
    1.28    | range_of (Delimfix (_, range)) = range