--- a/src/HOL/HOLCF/Tools/domaindef.ML Fri Aug 12 07:13:12 2011 -0700
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Fri Aug 12 07:18:28 2011 -0700
@@ -109,7 +109,7 @@
|> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
(*set*)
- val set = @{term "defl_set :: udom defl => udom => bool"} $ defl
+ val set = @{term "defl_set :: udom defl => udom set"} $ defl
(*pcpodef*)
val tac1 = rtac @{thm defl_set_bottom} 1
--- a/src/HOL/HOLCF/Tools/holcf_library.ML Fri Aug 12 07:13:12 2011 -0700
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML Fri Aug 12 07:18:28 2011 -0700
@@ -15,6 +15,7 @@
val boolT = HOLogic.boolT
val natT = HOLogic.natT
+val mk_setT = HOLogic.mk_setT
val mk_equals = Logic.mk_equals
val mk_eq = HOLogic.mk_eq
@@ -56,9 +57,9 @@
fun mk_lub t =
let
val T = Term.range_type (Term.fastype_of t)
- val lub_const = Const (@{const_name lub}, (T --> boolT) --> T)
+ val lub_const = Const (@{const_name lub}, mk_setT T --> T)
val UNIV_const = @{term "UNIV :: nat set"}
- val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT
+ val image_type = (natT --> T) --> mk_setT natT --> mk_setT T
val image_const = Const (@{const_name image}, image_type)
in
lub_const $ (image_const $ t $ UNIV_const)
--- a/src/HOL/Library/Infinite_Set.thy Fri Aug 12 07:13:12 2011 -0700
+++ b/src/HOL/Library/Infinite_Set.thy Fri Aug 12 07:18:28 2011 -0700
@@ -546,7 +546,7 @@
apply (induct n arbitrary: S)
apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
apply simp
-apply (metis Collect_def Collect_mem_eq DiffE infinite_remove)
+apply (metis Collect_mem_eq DiffE infinite_remove)
done
declare enumerate_0 [simp del] enumerate_Suc [simp del]