diff -r 6c8806696bed -r 56965d8e4e11 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu Aug 19 11:19:24 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Thu Aug 19 12:11:57 2010 +0200
@@ -658,7 +658,7 @@
       | Const (@{const_name Finite_Set.card}, _) => t
       | Const (@{const_name Finite_Set.finite}, _) => t
       | Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
-        Type ("fun", [@{typ nat}, Type ("bool", [])])])) => t
+        Type ("fun", [@{typ nat}, @{typ bool}])])) => t
       | Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
         Type ("fun", [@{typ nat}, @{typ nat}])])) => t
       | Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
@@ -835,7 +835,7 @@
       | Const (@{const_name Finite_Set.finite}, T) =>
         collect_type_axioms T axs
       | Const (@{const_name Orderings.less}, T as Type ("fun", [@{typ nat},
-        Type ("fun", [@{typ nat}, Type ("bool", [])])])) =>
+        Type ("fun", [@{typ nat}, @{typ bool}])])) =>
           collect_type_axioms T axs
       | Const (@{const_name Groups.plus}, T as Type ("fun", [@{typ nat},
         Type ("fun", [@{typ nat}, @{typ nat}])])) =>
@@ -2653,7 +2653,7 @@
   fun Finite_Set_card_interpreter thy model args t =
     case t of
       Const (@{const_name Finite_Set.card},
-        Type ("fun", [Type ("fun", [T, Type ("bool", [])]),
+        Type ("fun", [Type ("fun", [T, @{typ bool}]),
                       @{typ nat}])) =>
       let
         (* interpretation -> int *)
@@ -2685,7 +2685,7 @@
               Leaf (replicate size_of_nat False)
           end
         val set_constants =
-          make_constants thy model (Type ("fun", [T, Type ("bool", [])]))
+          make_constants thy model (Type ("fun", [T, HOLogic.boolT]))
       in
         SOME (Node (map card set_constants), model, args)
       end
@@ -2702,17 +2702,17 @@
   fun Finite_Set_finite_interpreter thy model args t =
     case t of
       Const (@{const_name Finite_Set.finite},
-        Type ("fun", [Type ("fun", [T, Type ("bool", [])]),
-                      Type ("bool", [])])) $ _ =>
+        Type ("fun", [Type ("fun", [T, @{typ bool}]),
+                      @{typ bool}])) $ _ =>
         (* we only consider finite models anyway, hence EVERY set is *)
         (* "finite"                                                  *)
         SOME (TT, model, args)
     | Const (@{const_name Finite_Set.finite},
-        Type ("fun", [Type ("fun", [T, Type ("bool", [])]),
-                      Type ("bool", [])])) =>
+        Type ("fun", [Type ("fun", [T, @{typ bool}]),
+                      @{typ bool}])) =>
       let
         val size_of_set =
-          size_of_type thy model (Type ("fun", [T, Type ("bool", [])]))
+          size_of_type thy model (Type ("fun", [T, HOLogic.boolT]))
       in
         (* we only consider finite models anyway, hence EVERY set is *)
         (* "finite"                                                  *)
@@ -2731,7 +2731,7 @@
   fun Nat_less_interpreter thy model args t =
     case t of
       Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
-        Type ("fun", [@{typ nat}, Type ("bool", [])])])) =>
+        Type ("fun", [@{typ nat}, @{typ bool}])])) =>
       let
         val size_of_nat = size_of_type thy model (@{typ nat})
         (* the 'n'-th nat is not less than the first 'n' nats, while it *)
@@ -2940,20 +2940,20 @@
   fun lfp_interpreter thy model args t =
     case t of
       Const (@{const_name lfp}, Type ("fun", [Type ("fun",
-        [Type ("fun", [T, Type ("bool", [])]),
-         Type ("fun", [_, Type ("bool", [])])]),
-         Type ("fun", [_, Type ("bool", [])])])) =>
+        [Type ("fun", [T, @{typ bool}]),
+         Type ("fun", [_, @{typ bool}])]),
+         Type ("fun", [_, @{typ bool}])])) =>
       let
         val size_elem = size_of_type thy model T
         (* the universe (i.e. the set that contains every element) *)
         val i_univ = Node (replicate size_elem TT)
         (* all sets with elements from type 'T' *)
         val i_sets =
-          make_constants thy model (Type ("fun", [T, Type ("bool", [])]))
+          make_constants thy model (Type ("fun", [T, HOLogic.boolT]))
         (* all functions that map sets to sets *)
         val i_funs = make_constants thy model (Type ("fun",
-          [Type ("fun", [T, Type ("bool", [])]),
-           Type ("fun", [T, Type ("bool", [])])]))
+          [Type ("fun", [T, @{typ bool}]),
+           Type ("fun", [T, @{typ bool}])]))
         (* "lfp(f) == Inter({u. f(u) <= u})" *)
         (* interpretation * interpretation -> bool *)
         fun is_subset (Node subs, Node sups) =
@@ -2995,20 +2995,20 @@
   fun gfp_interpreter thy model args t =
     case t of
       Const (@{const_name gfp}, Type ("fun", [Type ("fun",
-        [Type ("fun", [T, Type ("bool", [])]),
-         Type ("fun", [_, Type ("bool", [])])]),
-         Type ("fun", [_, Type ("bool", [])])])) =>
+        [Type ("fun", [T, @{typ bool}]),
+         Type ("fun", [_, @{typ bool}])]),
+         Type ("fun", [_, @{typ bool}])])) =>
       let
         val size_elem = size_of_type thy model T
         (* the universe (i.e. the set that contains every element) *)
         val i_univ = Node (replicate size_elem TT)
         (* all sets with elements from type 'T' *)
         val i_sets =
-          make_constants thy model (Type ("fun", [T, Type ("bool", [])]))
+          make_constants thy model (Type ("fun", [T, HOLogic.boolT]))
         (* all functions that map sets to sets *)
         val i_funs = make_constants thy model (Type ("fun",
-          [Type ("fun", [T, Type ("bool", [])]),
-           Type ("fun", [T, Type ("bool", [])])]))
+          [Type ("fun", [T, HOLogic.boolT]),
+           Type ("fun", [T, HOLogic.boolT])]))
         (* "gfp(f) == Union({u. u <= f(u)})" *)
         (* interpretation * interpretation -> bool *)
         fun is_subset (Node subs, Node sups) =