Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 42489 db9b9e46131c
parent 42361 23f352990944
child 42616 92715b528e78 
--- 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
isabelle