src/Pure/Isar/proof_context.ML

   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 mk_const: Proof.context -> string * typ list -> term
   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 transfer_syntax: theory -> Proof.context -> Proof.context

 
 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;
 
-fun mk_const ctxt (c, Ts) = Const (c, Consts.instance (consts_of ctxt) (c, Ts));
-
 val facts_of = #facts o rep_context;
 val cases_of = #cases o rep_context;
 
 
 (* theory transfer *)

     let
       val prt_term = Syntax.pretty_term ctxt;
 
       (*structures*)
       val structs = Local_Syntax.structs_of (syntax_of ctxt);
-      val prt_structs = if null structs then []
+      val prt_structs =
+        if null structs then []
         else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
           Pretty.commas (map Pretty.str structs))];
 
       (*fixes*)
       fun prt_fix (x, x') =
         if x = x' then Pretty.str x
         else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
       val fixes =
         rev (filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
           (Variable.fixes_of ctxt));
-      val prt_fixes = if null fixes then []
+      val prt_fixes =
+        if null fixes then []
         else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
           Pretty.commas (map prt_fix fixes))];
 
       (*prems*)
       val prems = Assumption.all_prems_of ctxt;
       val len = length prems;
       val suppressed = len - ! prems_limit;
-      val prt_prems = if null prems then []
+      val prt_prems =
+        if null prems then []
         else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @
           map (Display.pretty_thm ctxt) (drop suppressed prems))];
     in prt_structs @ prt_fixes @ prt_prems end;