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)