--- 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
--- 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')]));
--- 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'(_')))"),