src/HOL/Tools/datatype_prop.ML
changeset 13585 db4005b40cc6
parent 13465 08e3fe248ba9
child 13641 63d1790a43ed
--- a/src/HOL/Tools/datatype_prop.ML	Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Thu Sep 26 10:51:29 2002 +0200
@@ -168,7 +168,7 @@
 
 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;