src/Pure/primitive_defs.ML

     term -> (term * term) * term
   val abs_def: term -> term * term
   val mk_defpair: term * term -> string * term
 end;
 
-structure PrimitiveDefs: PRIMITIVE_DEFS =
+structure Primitive_Defs: PRIMITIVE_DEFS =
 struct
 
 fun term_kind (Const _) = "existing constant "
   | term_kind (Free _) = "free variable "
   | term_kind (Bound _) = "bound variable "