# HG changeset patch
# User wenzelm
# Date 1302287949 -7200
# Node ID 8fdbb3b10bebc5c80d7fe94c3ed948d06ef3a5ff
# Parent  0f4372a2d2e4ac35155583cb9675c8d8416bec39
moved CONST syntax/translations to their proper place;

diff -r 0f4372a2d2e4 -r 8fdbb3b10beb src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Apr 08 18:08:13 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Apr 08 20:39:09 2011 +0200
@@ -942,37 +942,6 @@
 end;
 
 
-(* authentic syntax *)
-
-local
-
-fun const_ast_tr intern ctxt [Ast.Variable c] =
-      let
-        val Const (c', _) = read_const_proper ctxt false c;
-        val d = if intern then Lexicon.mark_const c' else c;
-      in Ast.Constant d end
-  | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
-
-val typ = Simple_Syntax.read_typ;
-
-in
-
-val _ = Context.>> (Context.map_theory
- (Sign.add_syntax_i
-   [("_context_const", typ "id => logic", Delimfix "CONST _"),
-    ("_context_const", typ "id => aprop", Delimfix "CONST _"),
-    ("_context_const", typ "longid => logic", Delimfix "CONST _"),
-    ("_context_const", typ "longid => aprop", Delimfix "CONST _"),
-    ("_context_xconst", typ "id => logic", Delimfix "XCONST _"),
-    ("_context_xconst", typ "id => aprop", Delimfix "XCONST _"),
-    ("_context_xconst", typ "longid => logic", Delimfix "XCONST _"),
-    ("_context_xconst", typ "longid => aprop", Delimfix "XCONST _")] #>
-  Sign.add_advanced_trfuns
-    ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
-
-end;
-
-
 (* notation *)
 
 local
diff -r 0f4372a2d2e4 -r 8fdbb3b10beb src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 18:08:13 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 20:39:09 2011 +0200
@@ -660,10 +660,23 @@
   | type_constraint_tr' _ _ _ = raise Match;
 
 
+(* authentic syntax *)
+
+fun const_ast_tr intern ctxt [Ast.Variable c] =
+      let
+        val Const (c', _) = ProofContext.read_const_proper ctxt false c;
+        val d = if intern then Lexicon.mark_const c' else c;
+      in Ast.Constant d end
+  | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
+
+
 (* setup translations *)
 
 val _ = Context.>> (Context.map_theory
-  (Sign.add_advanced_trfunsT
+ (Sign.add_advanced_trfuns
+  ([("_context_const", const_ast_tr true),
+    ("_context_xconst", const_ast_tr false)], [], [], []) #>
+  Sign.add_advanced_trfunsT
    [("_type_prop", type_prop_tr'),
     ("\\<^const>TYPE", type_tr'),
     ("_type_constraint_", type_constraint_tr')]));
diff -r 0f4372a2d2e4 -r 8fdbb3b10beb src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Apr 08 18:08:13 2011 +0200
+++ b/src/Pure/pure_thy.ML	Fri Apr 08 20:39:09 2011 +0200
@@ -133,10 +133,18 @@
     ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
     ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     ("_update_name", typ "idt",                        NoSyn),
-    ("_constrainAbs", typ "'a",                       NoSyn),
+    ("_constrainAbs", typ "'a",                        NoSyn),
     ("_constrain_position", typ "id => id_position",   Delimfix "_"),
     ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
     ("_type_constraint_", typ "'a",                    NoSyn),
+    ("_context_const", typ "id => logic",              Delimfix "CONST _"),
+    ("_context_const", typ "id => aprop",              Delimfix "CONST _"),
+    ("_context_const", typ "longid => logic",          Delimfix "CONST _"),
+    ("_context_const", typ "longid => aprop",          Delimfix "CONST _"),
+    ("_context_xconst", typ "id => logic",             Delimfix "XCONST _"),
+    ("_context_xconst", typ "id => aprop",             Delimfix "XCONST _"),
+    ("_context_xconst", typ "longid => logic",         Delimfix "XCONST _"),
+    ("_context_xconst", typ "longid => aprop",         Delimfix "XCONST _"),
     (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
     (const Term.dummy_patternN, typ "aprop",           Delimfix "'_"),
     ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),