# HG changeset patch
# User blanchet
# Date 1390241125 -3600
# Node ID ec08a67e993b45f52621b685eb435b45af59102e
# Parent  558c9ceabaa107de58678efa4b805d8cabee9247
removed dependency of BNF package on Nitpick

diff -r 558c9ceabaa1 -r ec08a67e993b src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:59:53 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy	Mon Jan 20 19:05:25 2014 +0100
@@ -10,7 +10,7 @@
 header {* Shared Fixed Point Operations on Bounded Natural Functors *}
 
 theory BNF_FP_Base
-imports Nitpick BNF_Comp Ctr_Sugar
+imports BNF_Comp Ctr_Sugar
 begin
 
 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
diff -r 558c9ceabaa1 -r ec08a67e993b src/HOL/BNF_GFP.thy
--- a/src/HOL/BNF_GFP.thy	Mon Jan 20 18:59:53 2014 +0100
+++ b/src/HOL/BNF_GFP.thy	Mon Jan 20 19:05:25 2014 +0100
@@ -10,7 +10,7 @@
 header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
 
 theory BNF_GFP
-imports BNF_FP_Base List_Prefix
+imports BNF_FP_Base List_Prefix String
 keywords
   "codatatype" :: thy_decl and
   "primcorecursive" :: thy_goal and
diff -r 558c9ceabaa1 -r ec08a67e993b src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Jan 20 18:59:53 2014 +0100
+++ b/src/HOL/Main.thy	Mon Jan 20 19:05:25 2014 +0100
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction BNF_LFP BNF_GFP
+imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction Nitpick BNF_LFP BNF_GFP
 begin
 
 text {*
diff -r 558c9ceabaa1 -r ec08a67e993b src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jan 20 18:59:53 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jan 20 19:05:25 2014 +0100
@@ -1447,17 +1447,6 @@
            (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs),
            (unfoldN, unfold_thmss, K coiter_attrs)]
           |> massage_multi_notes;
-
-        fun is_codatatype (Type (s, _)) =
-            (case fp_sugar_of lthy s of SOME {fp = Greatest_FP, ...} => true | _ => false)
-          | is_codatatype _ = false;
-
-        val nitpick_supported = forall (is_codatatype o T_of_bnf) nested_bnfs;
-
-        fun register_nitpick fpT ({ctrs, casex, ...} : ctr_sugar) =
-          Nitpick_HOL.register_codatatype fpT (fst (dest_Const casex))
-            (map (dest_Const o mk_ctr As) ctrs)
-          |> Generic_Target.theory_declaration;
       in
         lthy
         |> Local_Theory.notes (common_notes @ notes) |> snd
@@ -1465,7 +1454,6 @@
           ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
           (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
           (transpose [sel_unfold_thmsss, sel_corec_thmsss])
-        |> nitpick_supported ? fold2 register_nitpick fpTs ctr_sugars
       end;
 
     val lthy'' = lthy'