changeset 56220 | 4c43a2881b25 |
parent 55890 | bd7927cca152 |
child 56254 | a2dd9200854d |
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Mar 19 21:59:31 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Mar 19 22:10:33 2014 +0100 @@ -148,7 +148,7 @@ fun nth_atom thy atomss pool for_auto T j = if for_auto then - Free (nth_atom_name thy atomss pool (hd (space_explode "." nitpick_prefix)) + Free (nth_atom_name thy atomss pool (hd (Long_Name.explode nitpick_prefix)) T j, T) else Const (nth_atom_name thy atomss pool "" T j, T)