src/Pure/consts.ML

   val alias: Name_Space.naming -> binding -> string -> T -> T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
   val intern_syntax: T -> xstring -> string
   val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
-  val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
+  val certify: Context.generic -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
   val declare: Context.generic -> binding * typ -> T -> T
   val constrain: string * typ option -> T -> T
   val abbreviate: Context.generic -> Type.tsig -> string -> binding * term -> T -> (term * term) * T

   in (Const (c, T), reports) end;
 
 
 (* certify *)
 
-fun certify pp tsig do_expand consts =
+fun certify context tsig do_expand consts =
   let
     fun err msg (c, T) =
       raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
-        Syntax.string_of_typ (Syntax.init_pretty pp) T, [], []);
+        Syntax.string_of_typ (Syntax.init_pretty context) T, [], []);
     val certT = Type.cert_typ tsig;
     fun cert tm =
       let
         val (head, args) = Term.strip_comb tm;
         val args' = map cert args;

 
 in
 
 fun abbreviate context tsig mode (b, raw_rhs) consts =
   let
-    val pp = Context.pretty_generic context;
-    val cert_term = certify pp tsig false consts;
-    val expand_term = certify pp tsig true consts;
+    val cert_term = certify context tsig false consts;
+    val expand_term = certify context tsig true consts;
     val force_expand = mode = Print_Mode.internal;
 
     val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
       error ("Illegal schematic variables on rhs of abbreviation " ^ Binding.print b);