--- a/src/Pure/Syntax/syntax.ML Sun Sep 16 17:58:59 2018 +0100
+++ b/src/Pure/Syntax/syntax.ML Sun Sep 16 20:33:37 2018 +0200
@@ -96,7 +96,6 @@
val print_gram: syntax -> unit
val print_trans: syntax -> unit
val print_syntax: syntax -> unit
- val guess_infix: syntax -> string -> mixfix option
datatype 'a trrule =
Parse_Rule of 'a * 'a |
Print_Rule of 'a * 'a |
@@ -608,17 +607,6 @@
end;
-(* reconstructing infixes -- educated guessing *)
-
-fun guess_infix (Syntax ({gram, ...}, _)) c =
- (case Parser.guess_infix_lr (Lazy.force gram) c of
- SOME (s, l, r, j) => SOME
- (if l then Infixl (Input.string s, j, Position.no_range)
- else if r then Infixr (Input.string s, j, Position.no_range)
- else Infix (Input.string s, j, Position.no_range))
- | NONE => NONE);
-
-
(** prepare translation rules **)