authentic syntax for *all* term constants;

--- a/src/Pure/Isar/proof_context.ML	Sun Feb 21 21:04:17 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Feb 21 21:08:25 2010 +0100
@@ -28,7 +28,6 @@
   val full_name: Proof.context -> binding -> string
   val syn_of: Proof.context -> Syntax.syntax
   val consts_of: Proof.context -> Consts.T
-  val const_syntax_name: Proof.context -> string -> string
   val the_const_constraint: Proof.context -> string -> typ
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
@@ -235,7 +234,6 @@
 val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
 
 val consts_of = #1 o #consts o rep_context;
-val const_syntax_name = Consts.syntax_name o consts_of;
 val the_const_constraint = Consts.the_constraint o consts_of;
 
 val facts_of = #facts o rep_context;
@@ -707,10 +705,10 @@
     val consts = consts_of ctxt;
   in
     t
-    |> Sign.extern_term (Consts.extern_early consts) thy
+    |> Sign.extern_term thy
     |> Local_Syntax.extern_term syntax
-    |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (Local_Syntax.syn_of syntax)
-        (not (PureThy.old_appl_syntax thy))
+    |> Syntax.standard_unparse_term (Consts.extern consts) ctxt
+        (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
   end;
 
 in
@@ -990,7 +988,7 @@
 fun const_ast_tr intern ctxt [Syntax.Variable c] =
       let
         val Const (c', _) = read_const_proper ctxt c;
-        val d = if intern then const_syntax_name ctxt c' else c;
+        val d = if intern then Syntax.constN ^ c' else c;
       in Syntax.Constant d end
   | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
 
@@ -1018,7 +1016,9 @@
 
 fun const_syntax _ (Free (x, T), mx) = SOME (true, (x, T, mx))
   | const_syntax ctxt (Const (c, _), mx) =
-      Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx))
+      (case try (Consts.type_scheme (consts_of ctxt)) c of
+        SOME T => SOME (false, (Syntax.constN ^ c, T, mx))
+      | NONE => NONE)
   | const_syntax _ _ = NONE;
 
 in

--- a/src/Pure/ML/ml_antiquote.ML	Sun Feb 21 21:04:17 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Sun Feb 21 21:08:25 2010 +0100
@@ -114,7 +114,7 @@
 
 fun const syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
   #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
-  |> syn ? ProofContext.const_syntax_name ctxt
+  |> syn ? prefix Syntax.constN
   |> ML_Syntax.print_string);
 
 val _ = inline "const_name" (const false);

--- a/src/Pure/Syntax/syn_trans.ML	Sun Feb 21 21:04:17 2010 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Sun Feb 21 21:08:25 2010 +0100
@@ -129,13 +129,15 @@
 
 (* type propositions *)
 
-fun mk_type ty = Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty);
+fun mk_type ty =
+  Lexicon.const "_constrain" $
+    Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "itself" $ ty);
 
 fun ofclass_tr (*"_ofclass"*) [ty, cls] = cls $ mk_type ty
   | ofclass_tr (*"_ofclass"*) ts = raise TERM ("ofclass_tr", ts);
 
 fun sort_constraint_tr (*"_sort_constraint"*) [ty] =
-      Lexicon.const "Pure.sort_constraint" $ mk_type ty
+      Lexicon.const "\\<^const>Pure.sort_constraint" $ mk_type ty
   | sort_constraint_tr (*"_sort_constraint"*) ts = raise TERM ("sort_constraint_tr", ts);
 
 
@@ -152,7 +154,7 @@
         (case Ast.unfold_ast_p "_asms" asms of
           (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
         | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
-      in Ast.fold_ast_p "==>" (prems, concl) end
+      in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end
   | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts);
 
 
@@ -350,7 +352,7 @@
 
 (* type propositions *)
 
-fun type_prop_tr' _ (*"_type_prop"*) T [Const ("Pure.sort_constraint", _)] =
+fun type_prop_tr' _ (*"_type_prop"*) T [Const ("\\<^const>Pure.sort_constraint", _)] =
       Lexicon.const "_sort_constraint" $ TypeExt.term_of_typ true T
   | type_prop_tr' show_sorts (*"_type_prop"*) T [t] =
       Lexicon.const "_ofclass" $ TypeExt.term_of_typ show_sorts T $ t
@@ -366,7 +368,7 @@
     fun is_prop Ts t =
       fastype_of1 (Ts, t) = propT handle TERM _ => false;
 
-    fun is_term (Const ("Pure.term", _) $ _) = true
+    fun is_term (Const ("\\<^const>Pure.term", _) $ _) = true
       | is_term _ = false;
 
     fun tr' _ (t as Const _) = t
@@ -379,7 +381,7 @@
       | tr' Ts (t as Bound _) =
           if is_prop Ts t then aprop t else t
       | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
-      | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
+      | tr' Ts (t as t1 $ (t2 as Const ("\\<^const>TYPE", Type ("itself", [T])))) =
           if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
           else tr' Ts t1 $ tr' Ts t2
       | tr' Ts (t as t1 $ t2) =
@@ -393,7 +395,7 @@
 fun impl_ast_tr' (*"==>"*) asts =
   if TypeExt.no_brackets () then raise Match
   else
-    (case Ast.unfold_ast_p "==>" (Ast.Appl (Ast.Constant "==>" :: asts)) of
+    (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
       (prems as _ :: _ :: _, concl) =>
         let
           val (asms, asm) = split_last prems;
@@ -514,11 +516,13 @@
    [("_abs", abs_ast_tr'),
     ("_idts", idtyp_ast_tr' "_idts"),
     ("_pttrns", idtyp_ast_tr' "_pttrns"),
-    ("==>", impl_ast_tr'),
+    ("\\<^const>==>", impl_ast_tr'),
     ("_index", index_ast_tr')]);
 
 val pure_trfunsT =
-  [("_type_prop", type_prop_tr'), ("TYPE", type_tr'), ("_type_constraint_", type_constraint_tr')];
+ [("_type_prop", type_prop_tr'),
+  ("\\<^const>TYPE", type_tr'),
+  ("_type_constraint_", type_constraint_tr')];
 
 fun struct_trfuns structs =
   ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);

--- a/src/Pure/consts.ML	Sun Feb 21 21:04:17 2010 +0100
+++ b/src/Pure/consts.ML	Sun Feb 21 21:08:25 2010 +0100
@@ -21,15 +21,13 @@
   val space_of: T -> Name_Space.T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
+  val intern_syntax: T -> xstring -> string
   val extern: T -> string -> xstring
-  val extern_early: T -> string -> xstring
-  val syntax: T -> string * mixfix -> string * typ * mixfix
-  val syntax_name: T -> string -> string
   val read_const: T -> string -> term
   val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
-  val declare: bool -> Name_Space.naming -> binding * typ -> T -> T
+  val declare: Name_Space.naming -> binding * typ -> T -> T
   val constrain: string * typ option -> T -> T
   val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string ->
     binding * term -> T -> (term * term) * T
@@ -46,7 +44,7 @@
 
 (* datatype T *)
 
-type decl = {T: typ, typargs: int list list, authentic: bool};
+type decl = {T: typ, typargs: int list list};
 type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
 
 datatype T = Consts of
@@ -128,18 +126,10 @@
 val intern = Name_Space.intern o space_of;
 val extern = Name_Space.extern o space_of;
 
-fun extern_early consts c =
-  (case try (the_const consts) c of
-    SOME ({authentic = true, ...}, _) => Syntax.constN ^ c
-  | _ => extern consts c);
-
-fun syntax consts (c, mx) =
-  let
-    val ({T, authentic, ...}, _) = the_const consts c handle TYPE (msg, _, _) => error msg;
-    val c' = if authentic then Syntax.constN ^ c else Long_Name.base_name c;
-  in (c', T, mx) end;
-
-fun syntax_name consts c = #1 (syntax consts (c, NoSyn));
+fun intern_syntax consts name =
+  (case try (unprefix Syntax.constN) name of
+    SOME c => c
+  | NONE => intern consts name);
 
 
 (* read_const *)
@@ -231,10 +221,10 @@
 
 (* declarations *)
 
-fun declare authentic naming (b, declT) =
+fun declare naming (b, declT) =
   map_consts (fn (decls, constraints, rev_abbrevs) =>
     let
-      val decl = {T = declT, typargs = typargs_of declT, authentic = authentic};
+      val decl = {T = declT, typargs = typargs_of declT};
       val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
     in (decls', constraints, rev_abbrevs) end);
 
@@ -285,7 +275,7 @@
   in
     consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
       let
-        val decl = {T = T, typargs = typargs_of T, authentic = true};
+        val decl = {T = T, typargs = typargs_of T};
         val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
         val (_, decls') = decls
           |> Name_Space.define true naming (b, (decl, SOME abbr));

--- a/src/Pure/pure_thy.ML	Sun Feb 21 21:04:17 2010 +0100
+++ b/src/Pure/pure_thy.ML	Sun Feb 21 21:08:25 2010 +0100
@@ -225,6 +225,7 @@
 
 val typ = Simple_Syntax.read_typ;
 val prop = Simple_Syntax.read_prop;
+val const = prefix Syntax.constN;
 
 val typeT = Syntax.typeT;
 val spropT = Syntax.spropT;
@@ -310,11 +311,11 @@
     ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
     ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     ("_update_name", typ "idt",                        NoSyn),
-    ("==>",         typ "prop => prop => prop",        Delimfix "op ==>"),
-    (Term.dummy_patternN, typ "aprop",                 Delimfix "'_"),
+    (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
+    (const Term.dummy_patternN, typ "aprop",           Delimfix "'_"),
     ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
-    ("Pure.term",   typ "logic => prop",               Delimfix "TERM _"),
-    ("Pure.conjunction", typ "prop => prop => prop",   Infixr ("&&&", 2))]
+    (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
+    (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
   #> Sign.add_syntax_i applC_syntax
   #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
    [("fun",      typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
@@ -326,14 +327,14 @@
     ("_idtypdummy", typ "type => idt",         Mixfix ("'_()\\<Colon>_", [], 0)),
     ("_type_constraint_", typ "'a",            NoSyn),
     ("_lambda",  typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
-    ("==",       typ "'a => 'a => prop",       Infixr ("\\<equiv>", 2)),
-    ("all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
-    ("==>",      typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
+    (const "==", typ "'a => 'a => prop",       Infixr ("\\<equiv>", 2)),
+    (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
+    (const "==>", typ "prop => prop => prop",  Infixr ("\\<Longrightarrow>", 1)),
     ("_DDDOT",   typ "aprop",                  Delimfix "\\<dots>"),
     ("_bigimpl", typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
     ("_DDDOT",   typ "logic",                  Delimfix "\\<dots>")]
   #> Sign.add_modesyntax_i ("", false)
-   [("prop", typ "prop => prop", Mixfix ("_", [0], 0))]
+   [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
   #> Sign.add_modesyntax_i ("HTML", false)
    [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
   #> Sign.add_consts_i

--- a/src/Pure/sign.ML	Sun Feb 21 21:04:17 2010 +0100
+++ b/src/Pure/sign.ML	Sun Feb 21 21:08:25 2010 +0100
@@ -41,7 +41,6 @@
   val declared_tyname: theory -> string -> bool
   val declared_const: theory -> string -> bool
   val const_monomorphic: theory -> string -> bool
-  val const_syntax_name: theory -> string -> string
   val const_typargs: theory -> string * typ -> typ list
   val const_instance: theory -> string * typ list -> typ
   val mk_const: theory -> string * typ list -> term
@@ -59,7 +58,7 @@
   val intern_typ: theory -> typ -> typ
   val extern_typ: theory -> typ -> typ
   val intern_term: theory -> term -> term
-  val extern_term: (string -> xstring) -> theory -> term -> term
+  val extern_term: theory -> term -> term
   val intern_tycons: theory -> typ -> typ
   val arity_number: theory -> string -> int
   val arity_sorts: theory -> string -> sort -> sort list
@@ -226,7 +225,6 @@
 val the_const_type = Consts.the_type o consts_of;
 val const_type = try o the_const_type;
 val const_monomorphic = Consts.is_monomorphic o consts_of;
-val const_syntax_name = Consts.syntax_name o consts_of;
 val const_typargs = Consts.typargs o consts_of;
 val const_instance = Consts.instance o consts_of;
 
@@ -299,7 +297,7 @@
 val intern_typ = typ_mapping intern_class intern_type;
 val extern_typ = typ_mapping extern_class extern_type;
 val intern_term = term_mapping intern_class intern_type intern_const;
-fun extern_term h = term_mapping extern_class extern_type (K h);
+val extern_term = term_mapping extern_class extern_type (fn _ => fn c => Syntax.constN ^ c);
 val intern_tycons = typ_mapping (K I) intern_type;
 
 end;
@@ -486,7 +484,10 @@
 fun notation add mode args thy =
   let
     val change_gram = if add then Syntax.update_const_gram else Syntax.remove_const_gram;
-    fun const_syntax (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx)
+    fun const_syntax (Const (c, _), mx) =
+          (case try (Consts.type_scheme (consts_of thy)) c of
+            SOME T => SOME (Syntax.constN ^ c, T, mx)
+          | NONE => NONE)
       | const_syntax _ = NONE;
   in gen_syntax change_gram (K I) mode (map_filter const_syntax args) thy end;
 
@@ -495,14 +496,14 @@
 
 local
 
-fun gen_add_consts parse_typ authentic raw_args thy =
+fun gen_add_consts parse_typ raw_args thy =
   let
     val ctxt = ProofContext.init thy;
     val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
     fun prep (b, raw_T, mx) =
       let
         val c = full_name thy b;
-        val c_syn = if authentic then Syntax.constN ^ c else Name.of_binding b;
+        val c_syn = Syntax.constN ^ c;
         val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
           cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
         val T' = Logic.varifyT T;
@@ -510,20 +511,20 @@
     val args = map prep raw_args;
   in
     thy
-    |> map_consts (fold (Consts.declare authentic (naming_of thy) o #1) args)
+    |> map_consts (fold (Consts.declare (naming_of thy) o #1) args)
     |> add_syntax_i (map #2 args)
     |> pair (map #3 args)
   end;
 
 in
 
-fun add_consts args = snd o gen_add_consts Syntax.parse_typ false args;
-fun add_consts_i args = snd o gen_add_consts (K I) false args;
+fun add_consts args = snd o gen_add_consts Syntax.parse_typ args;
+fun add_consts_i args = snd o gen_add_consts (K I) args;
 
 fun declare_const ((b, T), mx) thy =
   let
     val pos = Binding.pos_of b;
-    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true [(b, T, mx)] thy;
+    val ([const as Const (c, _)], thy') = gen_add_consts (K I) [(b, T, mx)] thy;
     val _ = Position.report (Markup.const_decl c) pos;
   in (const, thy') end;