src/HOL/Tools/datatype_rep_proofs.ML
changeset 13585 db4005b40cc6
parent 13340 9b0332344ae2
child 13641 63d1790a43ed
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Sep 26 10:51:29 2002 +0200
@@ -55,7 +55,7 @@
     val Numb_name = "Datatype_Universe.Numb";
     val Lim_name = "Datatype_Universe.Lim";
     val Funs_name = "Datatype_Universe.Funs";
-    val o_name = "Fun.op o";
+    val o_name = "Fun.comp";
     val sum_case_name = "Datatype.sum.sum_case";
 
     val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,