--- a/Nominal/nominal_function.ML	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_function.ML	Thu Jul 09 02:32:46 2015 +0100
@@ -27,9 +27,6 @@
     (Attrib.binding * string) list ->  Nominal_Function_Common.nominal_function_config ->
     bool -> local_theory -> Proof.state
 
-  val setup : theory -> theory
-  val get_congs : Proof.context -> thm list
-
   val get_info : Proof.context -> term -> nominal_info
 end
 
@@ -106,10 +103,10 @@
 val simp_attribs = map (Attrib.internal o K)
   [Simplifier.simp_add,
    Code.add_default_eqn_attribute,
-   Nitpick_Simps.add]
+   Named_Theorems.add @{named_theorems nitpick_simp}]
 
 val psimp_attribs = map (Attrib.internal o K)
-  [Nitpick_Psimps.add]
+  [Named_Theorems.add @{named_theorems nitpick_psimp}]
 
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
 
@@ -159,19 +156,19 @@
         val fnames = map (fst o fst) fixes
         fun qualify n = Binding.name n
           |> Binding.qualify true defname
-        val conceal_partial = if partials then I else Binding.conceal
+        val concealed_partial = if partials then I else Binding.concealed
 
         val addsmps = add_simps fnames post sort_cont
 
         val (((psimps', pinducts'), (_, [termination'])), lthy) =
           lthy
-          |> addsmps (conceal_partial o Binding.qualify false "partial")
-               "psimps" conceal_partial psimp_attribs psimps
-          ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
+          |> addsmps (concealed_partial o Binding.qualify false "partial")
+               "psimps" concealed_partial psimp_attribs psimps
+          ||>> Local_Theory.note ((concealed_partial (qualify "pinduct"),
                  [Attrib.internal (K (Rule_Cases.case_names cnames)),
                   Attrib.internal (K (Rule_Cases.consumes 1)),
                   Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
-          ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
+          ||>> Local_Theory.note ((Binding.concealed (qualify "termination"), []), [termination])
           ||> (snd o Local_Theory.note ((qualify "cases",
                  [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
           ||> (case domintros of NONE => I | SOME thms => 
@@ -216,7 +213,7 @@
       prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy
   in
     lthy'
-    |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
+    |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]]
     |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
   end
 
@@ -225,31 +222,6 @@
 fun nominal_function_cmd a b c int = 
   gen_nominal_function int Specification.read_spec "_::type" a b c
 
-
-fun add_case_cong n thy =
-  let
-    val cong = #case_cong (Datatype.the_info thy n)
-      |> safe_mk_meta_eq
-  in
-    Context.theory_map
-      (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
-  end
-
-val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
-
-
-
-(* setup *)
-
-val setup =
-  Attrib.setup @{binding fundef_cong}
-    (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
-    "declaration of congruence rule for function definitions"
-  #> setup_case_cong
-  #> Function_Common.Termination_Simps.setup
-
-val get_congs = Function_Ctx_Tree.get_function_congs
-
 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
   |> the_single |> snd
 
@@ -275,7 +247,7 @@
 
 (* nominal *)
 val _ =
-  Outer_Syntax.local_theory_to_proof' @{command_spec "nominal_function"}
+  Outer_Syntax.local_theory_to_proof' @{command_keyword nominal_function}
     "define general recursive nominal functions"
        (nominal_function_parser nominal_default_config
           >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))