--- a/src/Pure/Syntax/syntax.ML Tue Apr 26 17:23:21 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Tue Apr 26 21:05:52 2011 +0200
@@ -7,9 +7,6 @@
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
@@ -143,16 +140,14 @@
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 **)
@@ -750,5 +745,8 @@
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;