src/HOL/Tools/Nitpick/nitpick_model.ML
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)