src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 57631 959caab43a3d
parent 57629 e88b5f59cade
child 57633 4ff8c090d580
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
     1.3 @@ -1011,7 +1011,7 @@
     1.4                       (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
     1.5                       (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
     1.6                    I)
     1.7 -          |> Local_Theory.notes (anonymous_notes @ notes)
     1.8 +          |> Local_Theory.notes (anonymous_notes @ notes);
     1.9  
    1.10          val ctr_sugar =
    1.11            {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,