# HG changeset patch
# User blanchet
# Date 1392795274 -3600
# Node ID 315dd59201140f8daa2b03c19f55d85430c4f08a
# Parent  a5e33e18fb5c06f2d9c03e170d7f2ab73d65ed7b
adapted Nitpick to 'primrec' refactoring

diff -r a5e33e18fb5c -r 315dd5920114 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Feb 19 08:34:33 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Feb 19 08:34:34 2014 +0100
@@ -24,8 +24,8 @@
      get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) ->
       (term * term list list) list list -> local_theory ->
       typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
-     rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list -> term ->
-       term -> term -> term};
+     rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
+       term -> term -> term -> term};
 
   exception PRIMREC of string * term list;
 
@@ -95,8 +95,8 @@
    get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) ->
     (term * term list list) list list -> local_theory ->
     typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
-   rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list -> term ->
-     term -> term -> term};
+   rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
+     term -> term -> term -> term};
 
 structure Data = Theory_Data
 (
diff -r a5e33e18fb5c -r 315dd5920114 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 19 08:34:33 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 19 08:34:34 2014 +0100
@@ -656,7 +656,7 @@
 
 fun is_codatatype ctxt (Type (s, _)) =
     Option.map #fp (BNF_FP_Def_Sugar.fp_sugar_of ctxt s)
-        = SOME BNF_FP_Util.Greatest_FP orelse
+        = SOME BNF_Util.Greatest_FP orelse
     not (null (these (Option.map snd (AList.lookup (op =)
                             (#codatatypes (Data.get (Context.Proof ctxt))) s))))
   | is_codatatype _ _ = false
@@ -790,7 +790,7 @@
         |> Option.map snd |> these
       val ctrs2 =
         (case BNF_FP_Def_Sugar.fp_sugar_of ctxt co_s of
-           SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) =>
+           SOME (fp_sugar as {fp = BNF_Util.Greatest_FP, ...}) =>
            map dest_Const (#ctrs (#ctr_sugar fp_sugar))
          | _ => [])
     in
@@ -934,7 +934,7 @@
        SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type T)) xs'
      | _ =>
        (case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of
-          SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) =>
+          SOME (fp_sugar as {fp = BNF_Util.Greatest_FP, ...}) =>
           map (apsnd (repair_constr_type T) o dest_Const)
               (#ctrs (#ctr_sugar fp_sugar))
         | _ =>
@@ -1465,7 +1465,7 @@
                 (Datatype.get_all thy) [] @
     map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) @
     map_filter (fn {fp, ctr_sugar = {casex, ...}, ...} =>
-                   if fp = BNF_FP_Util.Greatest_FP then
+                   if fp = BNF_Util.Greatest_FP then
                      SOME (apsnd num_binder_types (dest_Const casex))
                    else
                      NONE)