updated to named_theorems;

--- a/src/HOL/HOL.thy	Sat Aug 16 21:11:08 2014 +0200
+++ b/src/HOL/HOL.thy	Sat Aug 16 22:14:57 2014 +0200
@@ -1921,35 +1921,14 @@
 
 subsubsection {* Nitpick setup *}
 
-ML {*
-structure Nitpick_Unfolds = Named_Thms
-(
-  val name = @{binding nitpick_unfold}
-  val description = "alternative definitions of constants as needed by Nitpick"
-)
-structure Nitpick_Simps = Named_Thms
-(
-  val name = @{binding nitpick_simp}
-  val description = "equational specification of constants as needed by Nitpick"
-)
-structure Nitpick_Psimps = Named_Thms
-(
-  val name = @{binding nitpick_psimp}
-  val description = "partial equational specification of constants as needed by Nitpick"
-)
-structure Nitpick_Choice_Specs = Named_Thms
-(
-  val name = @{binding nitpick_choice_spec}
-  val description = "choice specification of constants as needed by Nitpick"
-)
-*}
-
-setup {*
-  Nitpick_Unfolds.setup
-  #> Nitpick_Simps.setup
-  #> Nitpick_Psimps.setup
-  #> Nitpick_Choice_Specs.setup
-*}
+named_theorems nitpick_unfold
+  "alternative definitions of constants as needed by Nitpick"
+named_theorems nitpick_simp
+  "equational specification of constants as needed by Nitpick"
+named_theorems nitpick_psimp
+  "partial equational specification of constants as needed by Nitpick"
+named_theorems nitpick_choice_spec
+  "choice specification of constants as needed by Nitpick"
 
 declare if_bool_eq_conj [nitpick_unfold, no_atp]
         if_bool_eq_disj [no_atp]

--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Aug 16 21:11:08 2014 +0200
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Aug 16 22:14:57 2014 +0200
@@ -258,7 +258,8 @@
     thy2
     |> Sign.add_path (space_implode "_" new_type_names)
     |> Global_Theory.note_thmss ""
-      [((Binding.name "rec", [Nitpick_Simps.add]), [(rec_thms, [])])]
+      [((Binding.name "rec", [Named_Theorems.add @{named_theorems nitpick_simp}]),
+          [(rec_thms, [])])]
     ||> Sign.parent_path
     |-> (fn thms => pair (reccomb_names, maps #2 thms))
   end;
@@ -347,7 +348,8 @@
     val case_names = map case_name_of case_thms;
   in
     thy2
-    |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
+    |> Context.theory_map
+        ((fold o fold) (Named_Theorems.add_thm @{named_theorems nitpick_simp}) case_thms)
     |> Sign.parent_path
     |> Datatype_Aux.store_thmss "case" new_type_names case_thms
     |-> (fn thmss => pair (thmss, case_names))

--- a/src/HOL/Tools/Function/size.ML	Sat Aug 16 21:11:08 2014 +0200
+++ b/src/HOL/Tools/Function/size.ML	Sat Aug 16 22:14:57 2014 +0200
@@ -200,7 +200,7 @@
         val ([(_, size_thms)], thy'') = thy'
           |> Global_Theory.note_thmss ""
             [((Binding.name "size",
-                [Simplifier.simp_add, Nitpick_Simps.add,
+                [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp},
                  Thm.declaration_attribute (fn thm =>
                    Context.mapping (Code.add_default_eqn thm) I)]),
               [(size_eqns, [])])];

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Aug 16 21:11:08 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Aug 16 22:14:57 2014 +0200
@@ -1927,12 +1927,13 @@
     Const (s, _) => (s, t)
   | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
 
-fun def_table_for get ctxt subst =
-  ctxt |> get |> map (pair_for_prop o subst_atomic subst)
+fun def_table_for ts subst =
+  ts |> map (pair_for_prop o subst_atomic subst)
        |> AList.group (op =) |> Symtab.make
 
 fun const_def_tables ctxt subst ts =
-  (def_table_for (map prop_of o Nitpick_Unfolds.get) ctxt subst,
+  (def_table_for
+    (map prop_of (rev (Named_Theorems.get ctxt @{named_theorems nitpick_unfold}))) subst,
    fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
         (map pair_for_prop ts) Symtab.empty)
 
@@ -1943,14 +1944,15 @@
 
 fun const_simp_table ctxt =
   def_table_for (map_filter (equationalize_term ctxt "nitpick_simp" o prop_of)
-                 o Nitpick_Simps.get) ctxt
+    (rev (Named_Theorems.get ctxt @{named_theorems nitpick_simp})))
 
 fun const_psimp_table ctxt =
   def_table_for (map_filter (equationalize_term ctxt "nitpick_psimp" o prop_of)
-                 o Nitpick_Psimps.get) ctxt
+    (rev (Named_Theorems.get ctxt @{named_theorems nitpick_psimp})))
 
 fun const_choice_spec_table ctxt subst =
-  map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
+  map (subst_atomic subst o prop_of)
+    (rev (Named_Theorems.get ctxt @{named_theorems nitpick_choice_spec}))
   |> const_nondef_table
 
 fun inductive_intro_table ctxt subst def_tables =
@@ -1958,9 +1960,8 @@
     def_table_for
         (maps (map (unfold_mutually_inductive_preds thy def_tables o prop_of)
                o snd o snd)
-         o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
-                                  cat = Spec_Rules.Co_Inductive)
-         o Spec_Rules.get) ctxt subst
+         (filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
+                                 cat = Spec_Rules.Co_Inductive) (Spec_Rules.get ctxt))) subst
   end
 
 fun ground_theorem_table thy =

--- a/src/HOL/Tools/recdef.ML	Sat Aug 16 21:11:08 2014 +0200
+++ b/src/HOL/Tools/recdef.ML	Sat Aug 16 22:14:57 2014 +0200
@@ -202,7 +202,8 @@
       tfl_fn not_permissive ctxt congs wfs name R eqs thy;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     val simp_att =
-      if null tcs then [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]
+      if null tcs then [Simplifier.simp_add,
+        Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute]
       else [];
     val ((simps' :: rules', [induct']), thy) =
       thy