diff -r 4638622bcaa1 -r db9b9e46131c src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Apr 27 17:58:45 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Apr 27 19:39:50 2011 +0200 @@ -956,7 +956,7 @@ 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