diff --git a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
@@ -1,196 +1,196 @@
 theory Needham_Schroeder_Base
 imports Main "HOL-Library.Predicate_Compile_Quickcheck"
 begin
 
 datatype agent = Alice | Bob | Spy
 
 definition agents :: "agent set"
 where
   "agents = {Spy, Alice, Bob}"
 
 definition bad :: "agent set"
 where
   "bad = {Spy}"
 
 datatype key = pubEK agent | priEK agent
 
 fun invKey
 where
   "invKey (pubEK A) = priEK A"
 | "invKey (priEK A) = pubEK A"
 
 datatype
      msg = Agent  agent
          | Key    key
          | Nonce  nat
          | MPair  msg msg
          | Crypt  key msg
 
 syntax
   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
 translations
   "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
 
 inductive_set
   parts :: "msg set => msg set"
   for H :: "msg set"
   where
     Inj [intro]:               "X \<in> H ==> X \<in> parts H"
   | Fst:         "\<lbrace>X,Y\<rbrace>   \<in> parts H ==> X \<in> parts H"
   | Snd:         "\<lbrace>X,Y\<rbrace>   \<in> parts H ==> Y \<in> parts H"
   | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
 
 inductive_set
   analz :: "msg set => msg set"
   for H :: "msg set"
   where
     Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
   | Fst:     "\<lbrace>X,Y\<rbrace> \<in> analz H ==> X \<in> analz H"
   | Snd:     "\<lbrace>X,Y\<rbrace> \<in> analz H ==> Y \<in> analz H"
   | Decrypt [dest]: 
              "[|Crypt K X \<in> analz H; Key(invKey K) \<in> analz H|] ==> X \<in> analz H"
 
 inductive_set
   synth :: "msg set => msg set"
   for H :: "msg set"
   where
     Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
   | Agent  [intro]:   "Agent agt \<in> synth H"
   | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> \<lbrace>X,Y\<rbrace> \<in> synth H"
   | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
 
 primrec initState
 where
   initState_Alice:
     "initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)"
 | initState_Bob:
     "initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)"
 | initState_Spy:
     "initState Spy        =  (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)"
 
 datatype
   event = Says  agent agent msg
         | Gets  agent       msg
         | Notes agent       msg
 
 
 primrec knows :: "agent => event list => msg set"
 where
   knows_Nil:   "knows A [] = initState A"
 | knows_Cons:
     "knows A (ev # evs) =
        (if A = Spy then 
         (case ev of
            Says A' B X => insert X (knows Spy evs)
          | Gets A' X => knows Spy evs
          | Notes A' X  => 
              if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
         else
         (case ev of
            Says A' B X => 
              if A'=A then insert X (knows A evs) else knows A evs
          | Gets A' X    => 
              if A'=A then insert X (knows A evs) else knows A evs
          | Notes A' X    => 
              if A'=A then insert X (knows A evs) else knows A evs))"
 
 abbreviation (input)
   spies  :: "event list => msg set" where
   "spies == knows Spy"
 
 primrec used :: "event list => msg set"
 where
   used_Nil:   "used []         = \<Union>(parts ` initState ` agents)"
 | used_Cons:  "used (ev # evs) =
                      (case ev of
                         Says A B X => parts {X} \<union> used evs
                       | Gets A X   => used evs
                       | Notes A X  => parts {X} \<union> used evs)"
 
 subsection \<open>Preparations for sets\<close>
 
 fun find_first :: "('a => 'b option) => 'a list => 'b option"
 where
   "find_first f [] = None"
 | "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
 
 consts cps_of_set :: "'a set => ('a => term list option) => term list option"
 
 lemma
   [code]: "cps_of_set (set xs) f = find_first f xs"
 sorry
 
 consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
 consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
 
 lemma
   [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
 sorry
 
 consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
     => 'b list => 'a Quickcheck_Exhaustive.three_valued"
 
 lemma [code]:
   "find_first' f [] = Quickcheck_Exhaustive.No_value"
   "find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))"
 sorry
 
 lemma
   [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
 sorry
 
 setup \<open>
 let
   val Fun = Predicate_Compile_Aux.Fun
   val Input = Predicate_Compile_Aux.Input
   val Output = Predicate_Compile_Aux.Output
   val Bool = Predicate_Compile_Aux.Bool
   val oi = Fun (Output, Fun (Input, Bool))
   val ii = Fun (Input, Fun (Input, Bool))
-  fun of_set compfuns (Type ("fun", [T, _])) =
+  fun of_set compfuns \<^Type>\<open>fun T _\<close> =
     case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
-      Type ("Quickcheck_Exhaustive.three_valued", _) => 
-        Const(\<^const_name>\<open>neg_cps_of_set\<close>, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
-    | Type ("Predicate.pred", _) => Const(\<^const_name>\<open>pred_of_set\<close>, HOLogic.mk_setT T --> Predicate_Compile_Aux.mk_monadT compfuns T)
-    | _ => Const(\<^const_name>\<open>pos_cps_of_set\<close>, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
-  fun member compfuns (U as Type ("fun", [T, _])) =
-    (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
-      (Const (\<^const_name>\<open>Set.member\<close>, T --> HOLogic.mk_setT T --> \<^typ>\<open>bool\<close>) $ Bound 1 $ Bound 0))))
+      \<^Type>\<open>Quickcheck_Exhaustive.three_valued _\<close> => 
+        Const(\<^const_name>\<open>neg_cps_of_set\<close>, \<^Type>\<open>set T\<close> --> Predicate_Compile_Aux.mk_monadT compfuns T)
+    | Type ("Predicate.pred", _) => Const(\<^const_name>\<open>pred_of_set\<close>, \<^Type>\<open>set T\<close> --> Predicate_Compile_Aux.mk_monadT compfuns T)
+    | _ => Const(\<^const_name>\<open>pos_cps_of_set\<close>, \<^Type>\<open>set T\<close> --> Predicate_Compile_Aux.mk_monadT compfuns T)
+  fun member compfuns (U as \<^Type>\<open>fun T _\<close>) =
+    (absdummy T (absdummy \<^Type>\<open>set T\<close> (Predicate_Compile_Aux.mk_if compfuns
+      \<^Const>\<open>Set.member T for \<open>Bound 1\<close> \<open>Bound 0\<close>\<close>)))
  
 in
   Core_Data.force_modes_and_compilations \<^const_name>\<open>Set.member\<close>
     [(oi, (of_set, false)), (ii, (member, false))]
 end
 \<close>
 
 subsection \<open>Derived equations for analz, parts and synth\<close>
 
 lemma [code]:
   "analz H = (let
      H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y} | Crypt K X => if Key (invKey K) \<in> H then {X} else {} | _ => {}) ` H))
    in if H' = H then H else analz H')"
 sorry
 
 lemma [code]:
   "parts H = (let
      H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
    in if H' = H then H else parts H')"
 sorry
 
 definition synth' :: "msg set => msg => bool"
 where
   "synth' H m = (m \<in> synth H)"
 
 lemmas [code_pred_intro] = synth.intros[folded synth'_def]
 
 code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+
 
 setup \<open>Predicate_Compile_Data.ignore_consts [\<^const_name>\<open>analz\<close>, \<^const_name>\<open>knows\<close>]\<close>
 declare ListMem_iff[symmetric, code_pred_inline]
 declare [[quickcheck_timing]]
 
 setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
 declare [[quickcheck_full_support = false]]
 
 end
diff --git a/src/HOL/Quickcheck_Examples/Hotel_Example.thy b/src/HOL/Quickcheck_Examples/Hotel_Example.thy
--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy
@@ -1,193 +1,193 @@
 theory Hotel_Example
 imports Main "HOL-Library.Predicate_Compile_Quickcheck"
 begin
 
 datatype guest = Guest0 | Guest1
 datatype key = Key0 | Key1 | Key2 | Key3
 datatype room = Room0
 
 type_synonym card = "key * key"
 
 datatype event =
   Check_in guest room card
 | Enter guest room card
 | Exit guest room
 
 definition initk :: "room \<Rightarrow> key"
   where "initk = (%r. Key0)"
 
 declare initk_def[code_pred_def, code]
 
 primrec owns :: "event list \<Rightarrow> room \<Rightarrow> guest option"
 where
   "owns [] r = None"
 | "owns (e#s) r = (case e of
     Check_in g r' c \<Rightarrow> if r' = r then Some g else owns s r |
     Enter g r' c \<Rightarrow> owns s r |
     Exit g r' \<Rightarrow> owns s r)"
 
 primrec currk :: "event list \<Rightarrow> room \<Rightarrow> key"
 where
   "currk [] r = initk r"
 | "currk (e#s) r = (let k = currk s r in
     case e of Check_in g r' (k1, k2) \<Rightarrow> if r' = r then k2 else k
             | Enter g r' c \<Rightarrow> k
             | Exit g r \<Rightarrow> k)"
 
 primrec issued :: "event list \<Rightarrow> key set"
 where
   "issued [] = range initk"
 | "issued (e#s) = issued s \<union>
   (case e of Check_in g r (k1, k2) \<Rightarrow> {k2} | Enter g r c \<Rightarrow> {} | Exit g r \<Rightarrow> {})"
 
 primrec cards :: "event list \<Rightarrow> guest \<Rightarrow> card set"
 where
   "cards [] g = {}"
 | "cards (e#s) g = (let C = cards s g in
                     case e of Check_in g' r c \<Rightarrow> if g' = g then insert c C
                                                 else C
                             | Enter g r c \<Rightarrow> C
                             | Exit g r \<Rightarrow> C)"
 
 primrec roomk :: "event list \<Rightarrow> room \<Rightarrow> key"
 where
   "roomk [] r = initk r"
 | "roomk (e#s) r = (let k = roomk s r in
     case e of Check_in g r' c \<Rightarrow> k
             | Enter g r' (x,y) \<Rightarrow> if r' = r \<^cancel>\<open>\<and> x = k\<close> then y else k
             | Exit g r \<Rightarrow> k)"
 
 primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
 where
   "isin [] r = {}"
 | "isin (e#s) r = (let G = isin s r in
                  case e of Check_in g r c \<Rightarrow> G
                  | Enter g r' c \<Rightarrow> if r' = r then {g} \<union> G else G
                  | Exit g r' \<Rightarrow> if r'=r then G - {g} else G)"
 
 primrec hotel :: "event list \<Rightarrow> bool"
 where
   "hotel []  = True"
 | "hotel (e # s) = (hotel s & (case e of
   Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
   Enter g r (k,k') \<Rightarrow> (k,k') \<in> cards s g & (roomk s r \<in> {k, k'}) |
   Exit g r \<Rightarrow> g \<in> isin s r))"
 
 definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
 [code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
 
 definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
 where
   "feels_safe s r = (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'.
    s = s\<^sub>3 @ [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 \<and>
    no_Check_in (s\<^sub>3 @ s\<^sub>2) r \<and> isin (s\<^sub>2 @ [Check_in g r c] @ s\<^sub>1) r = {})"
 
 
 section \<open>Some setup\<close>
 
 lemma issued_nil: "issued [] = {Key0}"
 by (auto simp add: initk_def)
 
 lemmas issued_simps[code] = issued_nil issued.simps(2)
 
 
 setup \<open>Predicate_Compile_Data.ignore_consts [\<^const_name>\<open>Set.member\<close>,
   \<^const_name>\<open>issued\<close>, \<^const_name>\<open>cards\<close>, \<^const_name>\<open>isin\<close>,
   \<^const_name>\<open>Collect\<close>, \<^const_name>\<open>insert\<close>]\<close>
 ML_val \<open>Core_Data.force_modes_and_compilations\<close>
 
 fun find_first :: "('a => 'b option) => 'a list => 'b option"
 where
   "find_first f [] = None"
 | "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
 
 axiomatization cps_of_set :: "'a set => ('a => term list option) => term list option"
 where cps_of_set_code [code]: "cps_of_set (set xs) f = find_first f xs"
 
 axiomatization pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
 where pos_cps_of_set_code [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
 
 axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
     => 'b list => 'a Quickcheck_Exhaustive.three_valued"
 where find_first'_Nil: "find_first' f [] = Quickcheck_Exhaustive.No_value"
   and find_first'_Cons: "find_first' f (x # xs) =
     (case f (Quickcheck_Exhaustive.Known x) of
       Quickcheck_Exhaustive.No_value => find_first' f xs
     | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x
     | Quickcheck_Exhaustive.Unknown_value =>
         (case find_first' f xs of Quickcheck_Exhaustive.Value x =>
           Quickcheck_Exhaustive.Value x
         | _ => Quickcheck_Exhaustive.Unknown_value))"
 
 lemmas find_first'_code [code] = find_first'_Nil find_first'_Cons
 
 axiomatization neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
 where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
 
 setup \<open>
 let
   val Fun = Predicate_Compile_Aux.Fun
   val Input = Predicate_Compile_Aux.Input
   val Output = Predicate_Compile_Aux.Output
   val Bool = Predicate_Compile_Aux.Bool
   val oi = Fun (Output, Fun (Input, Bool))
   val ii = Fun (Input, Fun (Input, Bool))
-  fun of_set compfuns (Type ("fun", [T, _])) =
+  fun of_set compfuns \<^Type>\<open>fun T _\<close> =
     case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
-      Type ("Quickcheck_Exhaustive.three_valued", _) => 
-        Const(\<^const_name>\<open>neg_cps_of_set\<close>, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
-    | _ => Const(\<^const_name>\<open>pos_cps_of_set\<close>, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
-  fun member compfuns (U as Type ("fun", [T, _])) =
-    (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
-      (Const (\<^const_name>\<open>Set.member\<close>, T --> HOLogic.mk_setT T --> \<^typ>\<open>bool\<close>) $ Bound 1 $ Bound 0))))
+      \<^Type>\<open>Quickcheck_Exhaustive.three_valued _\<close> => 
+        Const(\<^const_name>\<open>neg_cps_of_set\<close>, \<^Type>\<open>set T\<close> --> Predicate_Compile_Aux.mk_monadT compfuns T)
+    | _ => Const(\<^const_name>\<open>pos_cps_of_set\<close>, \<^Type>\<open>set T\<close> --> Predicate_Compile_Aux.mk_monadT compfuns T)
+  fun member compfuns (U as \<^Type>\<open>fun T _\<close>) =
+    (absdummy T (absdummy \<^Type>\<open>set T\<close> (Predicate_Compile_Aux.mk_if compfuns
+      (\<^Const>\<open>Set.member T for \<open>Bound 1\<close> \<open>Bound 0\<close>\<close>))))
  
 in
   Core_Data.force_modes_and_compilations \<^const_name>\<open>Set.member\<close>
     [(oi, (of_set, false)), (ii, (member, false))]
 end
 \<close>
 section \<open>Property\<close>
 
 lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
 quickcheck[tester = exhaustive, size = 6, expect = counterexample]
 quickcheck[tester = smart_exhaustive, depth = 6, expect = counterexample]
 oops
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
 quickcheck[smart_exhaustive, depth = 10, allow_function_inversion, expect = counterexample]
 oops
 
 section \<open>Refinement\<close>
 
 fun split_list
 where
   "split_list [] = [([], [])]"
 | "split_list (z # zs) = (([], z # zs) # [(z # xs', ys'). (xs', ys') <- split_list zs])"
 
 lemma split_list: "((xs, ys) \<in> set (split_list zs)) = (zs = xs @ ys)"
 apply (induct zs arbitrary: xs ys)
 apply fastforce
 apply (case_tac xs)
 apply auto
 done
 
 lemma [code]: "no_Check_in s r = list_all (%x. case x of Check_in g r' c => r \<noteq> r' | _ => True) s"
 unfolding no_Check_in_def list_all_iff
 apply auto
 apply (case_tac x)
 apply auto
 done
 
 lemma [code]: "feels_safe s r = list_ex (%(s3, s2, s1, g, c, c'). no_Check_in (s3 @ s2) r &
     isin (s2 @ [Check_in g r c] @ s1) r = {}) ([(s3, s2, s1, g, c, c'). (s3, Enter g' r' c # r3) <- split_list s, r' = r, (s2, Check_in g r'' c' # s1) <- split_list r3, r'' = r, g = g'])"
 unfolding feels_safe_def list_ex_iff
 by auto (metis split_list)+
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
 (* quickcheck[exhaustive, size = 9, timeout = 2000] -- maybe possible with a lot of time *)
 quickcheck[narrowing, size = 7, expect = counterexample]
 oops
 
 end