# HG changeset patch
# User bulwahn
# Date 1301048340 -3600
# Node ID 17e0cd9bc259539652ca3971bf2ae7723653bbb7
# Parent  f5950b9760763a858ec1f9613edaf8c549564bc5
fixed postprocessing for term presentation in quickcheck; tuned spacing

diff -r f5950b976076 -r 17e0cd9bc259 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Mar 24 22:12:38 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Mar 25 11:19:00 2011 +0100
@@ -98,7 +98,7 @@
     fun map_Abs f t =
       case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) 
     fun process_args t = case strip_comb t of
-      (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
+      (c as Const (_, _), ts) => list_comb (c, map post_process_term ts)
   in
     case fastype_of t of
       Type (@{type_name fun}, [T1, T2]) =>
@@ -108,15 +108,15 @@
             |> (case T2 of
               @{typ bool} => 
                 (case t of
-                   Abs(_, _, @{const True}) => fst #> rev #> make_set T1
-                 | Abs(_, _, @{const False}) => fst #> rev #> make_coset T1
+                   Abs(_, _, @{const False}) => fst #> rev #> make_set T1
+                 | Abs(_, _, @{const True}) => fst #> rev #> make_coset T1
                  | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
                  | _ => raise TERM ("post_process_term", [t]))
             | Type (@{type_name option}, _) =>
                 (case t of
-                  Abs(_, _, Const(@{const_name None}, _)) => fst #> make_map T1 T2
+                  Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2
                 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
-                | _ => make_fun_upds T1 T2) 
+                | _ => make_fun_upds T1 T2)
             | _ => make_fun_upds T1 T2)
         | NONE => process_args t)
     | _ => process_args t