src/Pure/Syntax/syntax.ML

 (specified by mixfix declarations).
 *)
 
 signature SYNTAX =
 sig
-  val const: string -> term
-  val free: string -> term
-  val var: indexname -> term
   type operations
   val install_operations: operations -> unit
   val root: string Config.T
   val positions_raw: Config.raw
   val positions: bool Config.T

   val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
   val update_const_gram: bool -> (string -> bool) ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
   val update_trrules: Ast.ast trrule list -> syntax -> syntax
   val remove_trrules: Ast.ast trrule list -> syntax -> syntax
+  val const: string -> term
+  val free: string -> term
+  val var: indexname -> term
 end;
 
 structure Syntax: SYNTAX =
 struct
-
-val const = Lexicon.const;
-val free = Lexicon.free;
-val var = Lexicon.var;
-
 
 
 (** inner syntax operations **)
 
 (* back-patched operations *)

   (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
 
 val update_trrules = ext_syntax Syntax_Ext.syn_ext_rules o check_rules;
 val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
 
+
+open Lexicon.Syntax;
+
 end;