diff -r 74920496ab71 -r 08f3491c50bf src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 03 18:21:43 2013 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 03 19:58:00 2013 +0200 @@ -456,7 +456,7 @@ provide a hint to the user. *) fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) = not (null fixes) andalso - exists (String.isSuffix ".hyps" o fst) assumes andalso + exists (String.isSuffix ".hyps" o Name_Space.full_name Name_Space.default_naming o fst) assumes andalso exists (exists (curry (op =) name o shortest_name o fst) o datatype_constrs hol_ctxt) deep_dataTs val likely_in_struct_induct_step =