src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 58182 82478e6c60cb
parent 58177 166131276380
child 58185 e6e3b20340be
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Sep 04 09:02:43 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Sep 04 11:20:59 2014 +0200
     1.3 @@ -1025,7 +1025,7 @@
     1.4                       (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
     1.5                    I)
     1.6            |> Local_Theory.notes (anonymous_notes @ notes)
     1.7 -          (* for "datatype_realizer.ML": *)
     1.8 +          (* for "old_datatype_realizer.ML": *)
     1.9            |>> name_noted_thms fcT_name exhaustN;
    1.10  
    1.11          val ctr_sugar =