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,