src/HOL/Tools/datatype_prop.ML

 
 (*************** characteristic equations for primrec combinator **************)
 
 fun make_primrecs new_type_names descr sorts thy =
   let
-    val o_name = "Fun.op o";
+    val o_name = "Fun.comp";
 
     val sign = Theory.sign_of thy;
 
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;