src/HOL/Tools/hologic.ML

 
 signature HOLOGIC =
 sig
   val typeS: sort
   val typeT: typ
-  val mk_id: typ -> term
+  val id_const: typ -> term
   val mk_comp: term * term -> term
   val boolN: string
   val boolT: typ
   val Trueprop: term
   val mk_Trueprop: term -> term

 val typeT = Type_Infer.anyT typeS;
 
 
 (* functions *)
 
-fun mk_id T = Const ("Fun.id", T --> T);
+fun id_const T = Const ("Fun.id", T --> T);
 
 fun mk_comp (f, g) =
   let
     val fT = fastype_of f;
     val gT = fastype_of g;