src/Pure/Syntax/syntax.ML

   val empty_syntax: syntax
   val merge_syntax: syntax * syntax -> syntax
   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 |
     Parse_Print_Rule of 'a * 'a
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule

 fun print_syntax syn = Pretty.writeln_chunks (pretty_gram syn @ pretty_trans syn);
 
 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 **)
 
 (* rules *)