# HG changeset patch
# User wenzelm
# Date 1631472018 -7200
# Node ID f7ee629b9beb0e61e9b02f99cea6c23de81d00fb
# Parent  6bc96f31cafd2c442daf65d20b123bf2e37247f4
more antiquotations;

diff -r 6bc96f31cafd -r f7ee629b9beb src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Sun Sep 12 20:37:15 2021 +0200
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Sun Sep 12 20:40:18 2021 +0200
@@ -148,15 +148,15 @@
   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>
diff -r 6bc96f31cafd -r f7ee629b9beb src/HOL/Quickcheck_Examples/Hotel_Example.thy
--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Sun Sep 12 20:37:15 2021 +0200
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Sun Sep 12 20:40:18 2021 +0200
@@ -132,14 +132,14 @@
   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>