src/HOL/Tools/record_package.ML
changeset 5210 54aaa779b6b4
parent 5201 fac6fea3b782
child 5212 2bc5b5cf0516
equal deleted inserted replaced
5209:a69fe5a61b6c 5210:54aaa779b6b4
    97 
    97 
    98 (** tuple operations **)
    98 (** tuple operations **)
    99 
    99 
   100 (* more type class *)
   100 (* more type class *)
   101 
   101 
   102 val moreS = ["more"];
   102 val moreS = ["Record.more"];
   103 
   103 
   104 
   104 
   105 (* types *)
   105 (* types *)
   106 
   106 
   107 fun mk_fieldT ((c, T), U) = Type (suffix field_typeN c, [T, U]);
   107 fun mk_fieldT ((c, T), U) = Type (suffix field_typeN c, [T, U]);