src/Pure/Isar/proof_context.ML

   val naming_of: Proof.context -> Name_Space.naming
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   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
   val facts_of: Proof.context -> Facts.T
   val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list

 val syn_of = Local_Syntax.syn_of o syntax_of;
 val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
 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;
 val cases_of = #cases o rep_context;
 

     val thy = theory_of ctxt;
     val syntax = syntax_of ctxt;
     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
 
 val _ = Syntax.install_operations

 local
 
 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);
 
 in
 

 
 local
 
 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
 
 fun notation add mode args ctxt =