src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 55079 ec08a67e993b
parent 55061 a0adf838e2d1
child 55093 a4eafd0db804
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jan 20 18:59:53 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jan 20 19:05:25 2014 +0100
     1.3 @@ -1447,17 +1447,6 @@
     1.4             (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs),
     1.5             (unfoldN, unfold_thmss, K coiter_attrs)]
     1.6            |> massage_multi_notes;
     1.7 -
     1.8 -        fun is_codatatype (Type (s, _)) =
     1.9 -            (case fp_sugar_of lthy s of SOME {fp = Greatest_FP, ...} => true | _ => false)
    1.10 -          | is_codatatype _ = false;
    1.11 -
    1.12 -        val nitpick_supported = forall (is_codatatype o T_of_bnf) nested_bnfs;
    1.13 -
    1.14 -        fun register_nitpick fpT ({ctrs, casex, ...} : ctr_sugar) =
    1.15 -          Nitpick_HOL.register_codatatype fpT (fst (dest_Const casex))
    1.16 -            (map (dest_Const o mk_ctr As) ctrs)
    1.17 -          |> Generic_Target.theory_declaration;
    1.18        in
    1.19          lthy
    1.20          |> Local_Theory.notes (common_notes @ notes) |> snd
    1.21 @@ -1465,7 +1454,6 @@
    1.22            ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
    1.23            (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
    1.24            (transpose [sel_unfold_thmsss, sel_corec_thmsss])
    1.25 -        |> nitpick_supported ? fold2 register_nitpick fpTs ctr_sugars
    1.26        end;
    1.27  
    1.28      val lthy'' = lthy'