# HG changeset patch
# User haftmann
# Date 1282212717 -7200
# Node ID 56965d8e4e1178c94ac3e206b6f754710922a98e
# Parent  6c8806696bed2328bf7a360cb86b70bbb7151bb7
use HOLogic.boolT and @{typ bool} more pervasively

diff -r 6c8806696bed -r 56965d8e4e11 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Aug 19 11:19:24 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Aug 19 12:11:57 2010 +0200
@@ -388,7 +388,6 @@
 
 val type_of = Term.type_of
 
-val boolT = Type("bool",[])
 val propT = Type("prop",[])
 
 fun mk_defeq name rhs thy =
@@ -1007,7 +1006,7 @@
 local
     val th = thm "not_def"
     val thy = theory_of_thm th
-    val pp = Thm.reflexive (cterm_of thy (Const(@{const_name "Trueprop"},boolT-->propT)))
+    val pp = Thm.reflexive (cterm_of thy (Const(@{const_name "Trueprop"},HOLogic.boolT-->propT)))
 in
 val not_elim_thm = Thm.combination pp th
 end
@@ -1773,7 +1772,7 @@
         val (info',tm') = disamb_term_from info tm
         val th = norm_hyps th
         val ct = cterm_of thy tm'
-        val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name "Not"},boolT-->boolT) $ tm')) th
+        val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name "Not"},HOLogic.boolT-->HOLogic.boolT) $ tm')) th
         val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
         val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
         val res = HOLThm(rens_of info',res1)
diff -r 6c8806696bed -r 56965d8e4e11 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Aug 19 11:19:24 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Aug 19 12:11:57 2010 +0200
@@ -52,7 +52,7 @@
 fun transform_ho_typ (T as Type ("fun", _)) =
   let
     val (Ts, T') = strip_type T
-  in if T' = @{typ "bool"} then T else (Ts @ [T']) ---> HOLogic.boolT end
+  in if T' = HOLogic.boolT then T else (Ts @ [T']) ---> HOLogic.boolT end
 | transform_ho_typ t = t
 
 fun transform_ho_arg arg = 
diff -r 6c8806696bed -r 56965d8e4e11 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Thu Aug 19 11:19:24 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Thu Aug 19 12:11:57 2010 +0200
@@ -98,7 +98,7 @@
   | is_atom (Const (@{const_name "op &"}, _) $ _ $ _)                                    = false
   | is_atom (Const (@{const_name "op |"}, _) $ _ $ _)                                    = false
   | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _)                                  = false
-  | is_atom (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false
+  | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
   | is_atom (Const (@{const_name "Not"}, _) $ _)                                         = false
   | is_atom _                                                              = true;
 
@@ -205,7 +205,7 @@
 	in
 		make_nnf_imp OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ x $ y) =
+  | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
@@ -239,7 +239,7 @@
 	in
 		make_nnf_not_imp OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ x $ y)) =
+  | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
diff -r 6c8806696bed -r 56965d8e4e11 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Thu Aug 19 11:19:24 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Aug 19 12:11:57 2010 +0200
@@ -351,11 +351,11 @@
       @{term "Pair :: term list option * (bool list * bool) => Random.seed => (term list option * (bool list * bool)) * Random.seed"};
     fun mk_assms_report i =
       HOLogic.mk_prod (@{term "None :: term list option"},
-        HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"}
-          (replicate i @{term "True"} @ replicate (length assms - i) @{term "False"}),
-        @{term "False"}))
+        HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT
+          (replicate i @{term True} @ replicate (length assms - i) @{term False}),
+        @{term False}))
     fun mk_concl_report b =
-      HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"} (replicate (length assms) @{term "True"}),
+      HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT (replicate (length assms) @{term True}),
         if b then @{term True} else @{term False})
     val If =
       @{term "If :: bool => term list option * (bool list * bool) => term list option * (bool list * bool) => term list option * (bool list * bool)"}
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) =