src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 58317 21fac057681e
parent 58289 eb93bc67d361
child 58335 a5a3b576fcfb
equal deleted inserted replaced
58316:18e6cb6a5297 58317:21fac057681e
  1031                   (add_ctr_code fcT_name (map (Morphism.typ phi) As)
  1031                   (add_ctr_code fcT_name (map (Morphism.typ phi) As)
  1032                      (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
  1032                      (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
  1033                      (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
  1033                      (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
  1034                   I)
  1034                   I)
  1035           |> Local_Theory.notes (anonymous_notes @ notes)
  1035           |> Local_Theory.notes (anonymous_notes @ notes)
  1036           (* for "old_datatype_realizer.ML": *)
  1036           (* for "datatype_realizer.ML": *)
  1037           |>> name_noted_thms fcT_name exhaustN;
  1037           |>> name_noted_thms fcT_name exhaustN;
  1038 
  1038 
  1039         val ctr_sugar =
  1039         val ctr_sugar =
  1040           {T = fcT, ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
  1040           {T = fcT, ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
  1041            nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
  1041            nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,