--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Aug 25 16:59:48 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Aug 25 16:59:48 2010 +0200
@@ -301,7 +301,9 @@
val prelude =
"#!/usr/bin/swipl -q -t main -f\n\n" ^
":- use_module(library('dialect/ciao/aggregates')).\n" ^
- ":- style_check(-singleton).\n\n" ^
+ ":- style_check(-singleton).\n" ^
+ ":- style_check(-discontiguous).\n" ^
+ ":- style_check(-atom).\n\n" ^
"main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
"main :- halt(1).\n"
@@ -433,7 +435,8 @@
HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"})))
in
- set_compr :: (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs)
+ mk_set_compr [] ts
+ (set_compr :: (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))
end
end
in