# HG changeset patch
# User wenzelm
# Date 1303925990 -7200
# Node ID db9b9e46131cf566bec11e043db95691e31e7097
# Parent  4638622bcaa1f743341b3cc76ea8930e533bee56
some adhoc renaming, to accomodate more strict checks of fixes (cf. 4638622bcaa1);

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
diff -r 4638622bcaa1 -r db9b9e46131c src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 27 17:58:45 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 27 19:39:50 2011 +0200
@@ -1902,7 +1902,7 @@
     val ((T, ts), statistics) = eval ctxt stats param_user_modes comp_options k t_compr
     val setT = HOLogic.mk_setT T
     val elems = HOLogic.mk_set T ts
-    val cont = Free ("...", setT)
+    val cont = Free ("dots", setT)  (* FIXME proper name!? *)
     (* check expected values *)
     val () =
       case raw_expected of