some adhoc renaming, to accomodate more strict checks of fixes (cf. 4638622bcaa1);
authorwenzelm
Wed Apr 27 19:39:50 2011 +0200 (2011-04-27)
changeset 42489db9b9e46131c
parent 42488 4638622bcaa1
child 42490 3633ecaaf3ef
some adhoc renaming, to accomodate more strict checks of fixes (cf. 4638622bcaa1);
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Apr 27 17:58:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Apr 27 19:39:50 2011 +0200
     1.3 @@ -956,7 +956,7 @@
     1.4      fun mk_insert x S =
     1.5        Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S 
     1.6      fun mk_set_compr in_insert [] xs =
     1.7 -       rev ((Free ("...", fastype_of t_compr)) ::
     1.8 +       rev ((Free ("dots", fastype_of t_compr)) ::  (* FIXME proper name!? *)
     1.9          (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))
    1.10        | mk_set_compr in_insert (t :: ts) xs =
    1.11          let
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 27 17:58:45 2011 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 27 19:39:50 2011 +0200
     2.3 @@ -1902,7 +1902,7 @@
     2.4      val ((T, ts), statistics) = eval ctxt stats param_user_modes comp_options k t_compr
     2.5      val setT = HOLogic.mk_setT T
     2.6      val elems = HOLogic.mk_set T ts
     2.7 -    val cont = Free ("...", setT)
     2.8 +    val cont = Free ("dots", setT)  (* FIXME proper name!? *)
     2.9      (* check expected values *)
    2.10      val () =
    2.11        case raw_expected of