# HG changeset patch
# User wenzelm
# Date 1537122817 -7200
# Node ID f0d4b1db0ea0712e0cb3b050a8257bf278908cca
# Parent  f108b3b67adac0d8930d5447f91edccf737692b6
unused;

diff -r f108b3b67ada -r f0d4b1db0ea0 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sun Sep 16 17:58:59 2018 +0100
+++ b/src/Pure/Syntax/parser.ML	Sun Sep 16 20:33:37 2018 +0200
@@ -18,7 +18,6 @@
   exception PARSETREE of parsetree
   val pretty_parsetree: parsetree -> Pretty.T
   val parse: gram -> string -> Lexicon.token list -> parsetree list
-  val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
   val branching_level: int Config.T
 end;
 
@@ -718,20 +717,4 @@
       | pts => pts);
   in r end;
 
-
-fun guess_infix_lr (Gram gram) c = (*based on educated guess*)
-  let
-    fun freeze a = map_range (curry Vector.sub a) (Vector.length a);
-    val prods = maps (prods_content o #2) (freeze (#prods gram));
-    fun guess (SOME ([Nonterminal (_, k), Terminal tok, Nonterminal (_, l)], _, j)) =
-          if Lexicon.is_literal tok then
-            if k = j andalso l = j + 1 then SOME (Lexicon.str_of_token tok, true, false, j)
-            else if k = j + 1 then if l = j then SOME (Lexicon.str_of_token tok, false, true, j)
-              else if l = j + 1 then SOME (Lexicon.str_of_token tok, false, false, j)
-              else NONE
-            else NONE
-          else NONE
-      | guess _ = NONE;
-  in guess (find_first (fn (_, s, _) => s = c) prods) end;
-
 end;
diff -r f108b3b67ada -r f0d4b1db0ea0 src/Pure/Syntax/syntax.ML
--- 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 **)