# HG changeset patch
# User bulwahn
# Date 1282748388 -7200
# Node ID 9c9d1482738045da3a909cf43978d5c4ea7362ec
# Parent  182b180e98041c86915834f579ce73a04c606f7f
improving output of set comprehensions; adding style_check flags

diff -r 182b180e9804 -r 9c9d14827380 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- 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