--- a/src/Pure/Syntax/mixfix.ML Wed Mar 30 14:52:23 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML Wed Mar 30 14:59:12 2016 +0200
@@ -22,7 +22,6 @@
include BASIC_MIXFIX
val is_empty: mixfix -> bool
val equal: mixfix * mixfix -> bool
- val set_range: Position.range -> mixfix -> mixfix
val range_of: mixfix -> Position.range
val pos_of: mixfix -> Position.T
val reset_pos: mixfix -> mixfix
@@ -65,17 +64,6 @@
| equal (Structure _, Structure _) = true
| equal _ = false;
-fun set_range range mx =
- (case mx of
- NoSyn => NoSyn
- | Mixfix (sy, ps, p, _) => Mixfix (sy, ps, p, range)
- | Delimfix (sy, _) => Delimfix (sy, range)
- | Infix (sy, p, _) => Infix (sy, p, range)
- | Infixl (sy, p, _) => Infixl (sy, p, range)
- | Infixr (sy, p, _) => Infixr (sy, p, range)
- | Binder (sy, p, q, _) => Binder (sy, p, q, range)
- | Structure _ => Structure range);
-
fun range_of NoSyn = Position.no_range
| range_of (Mixfix (_, _, _, range)) = range
| range_of (Delimfix (_, range)) = range