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