src/HOL/Tools/Predicate_Compile/code_prolog.ML

     val _ = tracing "Restoring terms..."
     val empty = Const("Orderings.bot_class.bot", fastype_of t_compr)
     fun mk_insert x S =
       Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S 
     fun mk_set_compr in_insert [] xs =
-       rev ((Free ("...", fastype_of t_compr)) ::
+       rev ((Free ("dots", fastype_of t_compr)) ::  (* FIXME proper name!? *)
         (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))
       | mk_set_compr in_insert (t :: ts) xs =
         let
           val frees = Term.add_frees t []
         in