src/HOL/Tools/datatype_prop.ML
changeset 13585 db4005b40cc6
parent 13465 08e3fe248ba9
child 13641 63d1790a43ed
     1.1 --- a/src/HOL/Tools/datatype_prop.ML	Thu Sep 26 10:43:43 2002 +0200
     1.2 +++ b/src/HOL/Tools/datatype_prop.ML	Thu Sep 26 10:51:29 2002 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4  
     1.5  fun make_primrecs new_type_names descr sorts thy =
     1.6    let
     1.7 -    val o_name = "Fun.op o";
     1.8 +    val o_name = "Fun.comp";
     1.9  
    1.10      val sign = Theory.sign_of thy;
    1.11