src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 57633 4ff8c090d580
parent 57631 959caab43a3d
child 57700 a2c4adb839a9
child 57830 2d0f0d6fdf3e
     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 @@ -629,14 +629,9 @@
     1.4  
     1.5      val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss;
     1.6  
     1.7 -    fun after_qed thmss lthy =
     1.8 +    fun after_qed ([exhaust_thm] :: thmss) lthy =
     1.9        let
    1.10 -        val ([exhaust_thm0], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss));
    1.11 -        (* for "datatype_realizer.ML": *)
    1.12 -        val exhaust_thm =
    1.13 -          Thm.name_derivation (fcT_name ^ Long_Name.separator ^ exhaustN) exhaust_thm0;
    1.14 -
    1.15 -        val inject_thms = flat inject_thmss;
    1.16 +        val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;
    1.17  
    1.18          val rho_As = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
    1.19  
    1.20 @@ -1011,7 +1006,9 @@
    1.21                       (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
    1.22                       (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
    1.23                    I)
    1.24 -          |> Local_Theory.notes (anonymous_notes @ notes);
    1.25 +          |> Local_Theory.notes (anonymous_notes @ notes)
    1.26 +          (* for "datatype_realizer.ML": *)
    1.27 +          |>> name_noted_thms fcT_name exhaustN;
    1.28  
    1.29          val ctr_sugar =
    1.30            {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,