src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -7,54 +7,54 @@
 structure Predicate_Comp_Funs =  (* FIXME proper signature *)
 struct
 
-fun mk_monadT T = Type (@{type_name Predicate.pred}, [T])
+fun mk_monadT T = Type (\<^type_name>\<open>Predicate.pred\<close>, [T])
 
-fun dest_monadT (Type (@{type_name Predicate.pred}, [T])) = T
+fun dest_monadT (Type (\<^type_name>\<open>Predicate.pred\<close>, [T])) = T
   | dest_monadT T = raise TYPE ("dest_monadT", [T], [])
 
-fun mk_empty T = Const (@{const_name Orderings.bot}, mk_monadT T)
+fun mk_empty T = Const (\<^const_name>\<open>Orderings.bot\<close>, mk_monadT T)
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name Predicate.single}, T --> mk_monadT T) $ t end
+  in Const(\<^const_name>\<open>Predicate.single\<close>, T --> mk_monadT T) $ t end
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Predicate.bind\<close>, fastype_of x --> T --> U) $ x $ f
   end
 
-val mk_plus = HOLogic.mk_binop @{const_name sup}
+val mk_plus = HOLogic.mk_binop \<^const_name>\<open>sup\<close>
 
-fun mk_if cond = Const (@{const_name Predicate.if_pred},
+fun mk_if cond = Const (\<^const_name>\<open>Predicate.if_pred\<close>,
   HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto T (f, from, to) =
-  list_comb (Const (@{const_name Predicate.iterate_upto},
-      [@{typ natural} --> T, @{typ natural}, @{typ natural}] ---> mk_monadT T),
+  list_comb (Const (\<^const_name>\<open>Predicate.iterate_upto\<close>,
+      [\<^typ>\<open>natural\<close> --> T, \<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>] ---> mk_monadT T),
     [f, from, to])
 
 fun mk_not t =
   let
     val T = mk_monadT HOLogic.unitT
-  in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
+  in Const (\<^const_name>\<open>Predicate.not_pred\<close>, T --> T) $ t end
 
 fun mk_Enum f =
   let val T as Type ("fun", [T', _]) = fastype_of f
   in
-    Const (@{const_name Predicate.Pred}, T --> mk_monadT T') $ f    
+    Const (\<^const_name>\<open>Predicate.Pred\<close>, T --> mk_monadT T') $ f    
   end;
 
 fun mk_Eval (f, x) =
   let
     val T = dest_monadT (fastype_of f)
   in
-    Const (@{const_name Predicate.eval}, mk_monadT T --> T --> HOLogic.boolT) $ f $ x
+    Const (\<^const_name>\<open>Predicate.eval\<close>, mk_monadT T --> T --> HOLogic.boolT) $ f $ x
   end
 
-fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)
+fun dest_Eval (Const (\<^const_name>\<open>Predicate.eval\<close>, _) $ f $ x) = (f, x)
 
-fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
+fun mk_map T1 T2 tf tp = Const (\<^const_name>\<open>Predicate.map\<close>,
   (T1 --> T2) --> mk_monadT T1 --> mk_monadT T2) $ tf $ tp
 
 val compfuns =
@@ -70,27 +70,27 @@
 struct
 
 fun mk_monadT T =
-  (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"}
+  (T --> \<^typ>\<open>Code_Evaluation.term list option\<close>) --> \<^typ>\<open>Code_Evaluation.term list option\<close>
 
 fun dest_monadT
-      (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T
+      (Type ("fun", [Type ("fun", [T, \<^typ>\<open>term list option\<close>]), \<^typ>\<open>term list option\<close>])) = T
   | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
 
-fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_monadT T)
+fun mk_empty T = Const (\<^const_name>\<open>Quickcheck_Exhaustive.cps_empty\<close>, mk_monadT T)
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_monadT T) $ t end
+  in Const(\<^const_name>\<open>Quickcheck_Exhaustive.cps_single\<close>, T --> mk_monadT T) $ t end
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Quickcheck_Exhaustive.cps_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Quickcheck_Exhaustive.cps_bind\<close>, fastype_of x --> T --> U) $ x $ f
   end
 
-val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus}
+val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Quickcheck_Exhaustive.cps_plus\<close>
 
-fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if},
+fun mk_if cond = Const (\<^const_name>\<open>Quickcheck_Exhaustive.cps_if\<close>,
   HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto _ _ = error "not implemented yet"
@@ -98,7 +98,7 @@
 fun mk_not t =
   let
     val T = mk_monadT HOLogic.unitT
-  in Const (@{const_name Quickcheck_Exhaustive.cps_not}, T --> T) $ t end
+  in Const (\<^const_name>\<open>Quickcheck_Exhaustive.cps_not\<close>, T --> T) $ t end
 
 fun mk_Enum _ = error "not implemented"
 
@@ -120,40 +120,40 @@
 structure Pos_Bounded_CPS_Comp_Funs =  (* FIXME proper signature *)
 struct
 
-val resultT = @{typ "(bool * Code_Evaluation.term list) option"}
-fun mk_monadT T = (T --> resultT) --> @{typ "natural"} --> resultT
+val resultT = \<^typ>\<open>(bool * Code_Evaluation.term list) option\<close>
+fun mk_monadT T = (T --> resultT) --> \<^typ>\<open>natural\<close> --> resultT
 
-fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "(bool * term list) option"}]),
-  @{typ "natural => (bool * term list) option"}])) = T
+fun dest_monadT (Type ("fun", [Type ("fun", [T, \<^typ>\<open>(bool * term list) option\<close>]),
+  \<^typ>\<open>natural => (bool * term list) option\<close>])) = T
   | dest_monadT T = raise TYPE ("dest_monadT", [T], [])
 
-fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_monadT T)
+fun mk_empty T = Const (\<^const_name>\<open>Quickcheck_Exhaustive.pos_bound_cps_empty\<close>, mk_monadT T)
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_monadT T) $ t end
+  in Const(\<^const_name>\<open>Quickcheck_Exhaustive.pos_bound_cps_single\<close>, T --> mk_monadT T) $ t end
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Quickcheck_Exhaustive.pos_bound_cps_bind\<close>, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus}
+val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Quickcheck_Exhaustive.pos_bound_cps_plus\<close>
 
 fun mk_if cond =
-  Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if},
+  Const (\<^const_name>\<open>Quickcheck_Exhaustive.pos_bound_cps_if\<close>,
     HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto _ _ = error "not implemented yet"
 
 fun mk_not t =
   let
-    val nT = @{typ "(unit Quickcheck_Exhaustive.unknown =>
+    val nT = \<^typ>\<open>(unit Quickcheck_Exhaustive.unknown =>
       Code_Evaluation.term list Quickcheck_Exhaustive.three_valued) => natural =>
-      Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
+      Code_Evaluation.term list Quickcheck_Exhaustive.three_valued\<close>
     val T = mk_monadT HOLogic.unitT
-  in Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_not}, nT --> T) $ t end
+  in Const (\<^const_name>\<open>Quickcheck_Exhaustive.pos_bound_cps_not\<close>, nT --> T) $ t end
 
 fun mk_Enum _ = error "not implemented"
 
@@ -176,31 +176,31 @@
 struct
 
 fun mk_monadT T =
-  (Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T])
-    --> @{typ "Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"})
-    --> @{typ "natural => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
+  (Type (\<^type_name>\<open>Quickcheck_Exhaustive.unknown\<close>, [T])
+    --> \<^typ>\<open>Code_Evaluation.term list Quickcheck_Exhaustive.three_valued\<close>)
+    --> \<^typ>\<open>natural => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued\<close>
 
 fun dest_monadT
-    (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]),
-      @{typ "term list Quickcheck_Exhaustive.three_valued"}]),
-      @{typ "natural => term list Quickcheck_Exhaustive.three_valued"}])) = T
+    (Type ("fun", [Type ("fun", [Type (\<^type_name>\<open>Quickcheck_Exhaustive.unknown\<close>, [T]),
+      \<^typ>\<open>term list Quickcheck_Exhaustive.three_valued\<close>]),
+      \<^typ>\<open>natural => term list Quickcheck_Exhaustive.three_valued\<close>])) = T
   | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
 
-fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_monadT T)
+fun mk_empty T = Const (\<^const_name>\<open>Quickcheck_Exhaustive.neg_bound_cps_empty\<close>, mk_monadT T)
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_monadT T) $ t end
+  in Const(\<^const_name>\<open>Quickcheck_Exhaustive.neg_bound_cps_single\<close>, T --> mk_monadT T) $ t end
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Quickcheck_Exhaustive.neg_bound_cps_bind\<close>, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus}
+val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Quickcheck_Exhaustive.neg_bound_cps_plus\<close>
 
-fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if},
+fun mk_if cond = Const (\<^const_name>\<open>Quickcheck_Exhaustive.neg_bound_cps_if\<close>,
   HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto _ _ = error "not implemented"
@@ -208,9 +208,9 @@
 fun mk_not t =
   let
     val T = mk_monadT HOLogic.unitT
-    val pT = @{typ "(unit => (bool * Code_Evaluation.term list) option)"}
-      --> @{typ "natural => (bool * Code_Evaluation.term list) option"}
-  in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end
+    val pT = \<^typ>\<open>(unit => (bool * Code_Evaluation.term list) option)\<close>
+      --> \<^typ>\<open>natural => (bool * Code_Evaluation.term list) option\<close>
+  in Const (\<^const_name>\<open>Quickcheck_Exhaustive.neg_bound_cps_not\<close>, pT --> T) $ t end
 
 fun mk_Enum _ = error "not implemented"
 
@@ -233,44 +233,44 @@
 struct
 
 fun mk_randompredT T =
-  @{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_monadT T, @{typ Random.seed})
+  \<^typ>\<open>Random.seed\<close> --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_monadT T, \<^typ>\<open>Random.seed\<close>)
 
-fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod},
-  [Type (@{type_name Predicate.pred}, [T]), @{typ Random.seed}])])) = T
+fun dest_randompredT (Type ("fun", [\<^typ>\<open>Random.seed\<close>, Type (\<^type_name>\<open>Product_Type.prod\<close>,
+  [Type (\<^type_name>\<open>Predicate.pred\<close>, [T]), \<^typ>\<open>Random.seed\<close>])])) = T
   | dest_randompredT T = raise TYPE ("dest_randompredT", [T], [])
 
-fun mk_empty T = Const(@{const_name Random_Pred.empty}, mk_randompredT T)
+fun mk_empty T = Const(\<^const_name>\<open>Random_Pred.empty\<close>, mk_randompredT T)
 
 fun mk_single t =
   let               
     val T = fastype_of t
   in
-    Const (@{const_name Random_Pred.single}, T --> mk_randompredT T) $ t
+    Const (\<^const_name>\<open>Random_Pred.single\<close>, T --> mk_randompredT T) $ t
   end
 
 fun mk_bind (x, f) =
   let
     val T as (Type ("fun", [_, U])) = fastype_of f
   in
-    Const (@{const_name Random_Pred.bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Random_Pred.bind\<close>, fastype_of x --> T --> U) $ x $ f
   end
 
-val mk_plus = HOLogic.mk_binop @{const_name Random_Pred.union}
+val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Random_Pred.union\<close>
 
-fun mk_if cond = Const (@{const_name Random_Pred.if_randompred},
+fun mk_if cond = Const (\<^const_name>\<open>Random_Pred.if_randompred\<close>,
   HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto T (f, from, to) =
-  list_comb (Const (@{const_name Random_Pred.iterate_upto},
-      [@{typ natural} --> T, @{typ natural}, @{typ natural}] ---> mk_randompredT T),
+  list_comb (Const (\<^const_name>\<open>Random_Pred.iterate_upto\<close>,
+      [\<^typ>\<open>natural\<close> --> T, \<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>] ---> mk_randompredT T),
     [f, from, to])
 
 fun mk_not t =
   let
     val T = mk_randompredT HOLogic.unitT
-  in Const (@{const_name Random_Pred.not_randompred}, T --> T) $ t end
+  in Const (\<^const_name>\<open>Random_Pred.not_randompred\<close>, T --> T) $ t end
 
-fun mk_map T1 T2 tf tp = Const (@{const_name Random_Pred.map},
+fun mk_map T1 T2 tf tp = Const (\<^const_name>\<open>Random_Pred.map\<close>,
   (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
 
 val compfuns =
@@ -285,36 +285,36 @@
 structure DSequence_CompFuns =  (* FIXME proper signature *)
 struct
 
-fun mk_dseqT T = Type ("fun", [@{typ natural}, Type ("fun", [@{typ bool},
-  Type (@{type_name Option.option}, [Type  (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])
+fun mk_dseqT T = Type ("fun", [\<^typ>\<open>natural\<close>, Type ("fun", [\<^typ>\<open>bool\<close>,
+  Type (\<^type_name>\<open>Option.option\<close>, [Type  (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>, [T])])])])
 
-fun dest_dseqT (Type ("fun", [@{typ natural}, Type ("fun", [@{typ bool},
-  Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
+fun dest_dseqT (Type ("fun", [\<^typ>\<open>natural\<close>, Type ("fun", [\<^typ>\<open>bool\<close>,
+  Type (\<^type_name>\<open>Option.option\<close>, [Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>, [T])])])])) = T
   | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
 
-fun mk_empty T = Const (@{const_name Limited_Sequence.empty}, mk_dseqT T);
+fun mk_empty T = Const (\<^const_name>\<open>Limited_Sequence.empty\<close>, mk_dseqT T);
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name Limited_Sequence.single}, T --> mk_dseqT T) $ t end;
+  in Const(\<^const_name>\<open>Limited_Sequence.single\<close>, T --> mk_dseqT T) $ t end;
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Limited_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Limited_Sequence.bind\<close>, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.union};
+val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Limited_Sequence.union\<close>;
 
-fun mk_if cond = Const (@{const_name Limited_Sequence.if_seq},
+fun mk_if cond = Const (\<^const_name>\<open>Limited_Sequence.if_seq\<close>,
   HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
 
 fun mk_not t = let val T = mk_dseqT HOLogic.unitT
-  in Const (@{const_name Limited_Sequence.not_seq}, T --> T) $ t end
+  in Const (\<^const_name>\<open>Limited_Sequence.not_seq\<close>, T --> T) $ t end
 
-fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.map},
+fun mk_map T1 T2 tf tp = Const (\<^const_name>\<open>Limited_Sequence.map\<close>,
   (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
 
 val compfuns =
@@ -330,37 +330,37 @@
 struct
 
 fun mk_pos_dseqT T =
-  @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
+  \<^typ>\<open>natural\<close> --> Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>, [T])
 
 fun dest_pos_dseqT
-      (Type ("fun", [@{typ natural}, Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T
+      (Type ("fun", [\<^typ>\<open>natural\<close>, Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>, [T])])) = T
   | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], [])
 
-fun mk_empty T = Const (@{const_name Limited_Sequence.pos_empty}, mk_pos_dseqT T)
+fun mk_empty T = Const (\<^const_name>\<open>Limited_Sequence.pos_empty\<close>, mk_pos_dseqT T)
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name Limited_Sequence.pos_single}, T --> mk_pos_dseqT T) $ t end
+  in Const(\<^const_name>\<open>Limited_Sequence.pos_single\<close>, T --> mk_pos_dseqT T) $ t end
 
 fun mk_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Limited_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Limited_Sequence.pos_bind\<close>, fastype_of x --> T --> U) $ x $ f
   end
   
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Limited_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Limited_Sequence.pos_decr_bind\<close>, fastype_of x --> T --> U) $ x $ f
   end
 
-val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.pos_union}
+val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Limited_Sequence.pos_union\<close>
 
 fun mk_if cond =
-  Const (@{const_name Limited_Sequence.pos_if_seq},
+  Const (\<^const_name>\<open>Limited_Sequence.pos_if_seq\<close>,
     HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
@@ -369,12 +369,12 @@
   let
     val pT = mk_pos_dseqT HOLogic.unitT
     val nT =
-      @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
-        [Type (@{type_name Option.option}, [@{typ unit}])])
-  in Const (@{const_name Limited_Sequence.pos_not_seq}, nT --> pT) $ t end
+      \<^typ>\<open>natural\<close> --> Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>,
+        [Type (\<^type_name>\<open>Option.option\<close>, [\<^typ>\<open>unit\<close>])])
+  in Const (\<^const_name>\<open>Limited_Sequence.pos_not_seq\<close>, nT --> pT) $ t end
 
 fun mk_map T1 T2 tf tp =
-  Const (@{const_name Limited_Sequence.pos_map},
+  Const (\<^const_name>\<open>Limited_Sequence.pos_map\<close>,
     (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns =
@@ -395,40 +395,40 @@
 structure New_Neg_DSequence_CompFuns =  (* FIXME proper signature *)
 struct
 
-fun mk_neg_dseqT T = @{typ natural} -->
-  Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
+fun mk_neg_dseqT T = \<^typ>\<open>natural\<close> -->
+  Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>, [Type (\<^type_name>\<open>Option.option\<close>, [T])])
 
 fun dest_neg_dseqT
-    (Type ("fun", [@{typ natural},
-      Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) =
+    (Type ("fun", [\<^typ>\<open>natural\<close>,
+      Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>, [Type (\<^type_name>\<open>Option.option\<close>, [T])])])) =
       T
   | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], [])
 
-fun mk_empty T = Const (@{const_name Limited_Sequence.neg_empty}, mk_neg_dseqT T)
+fun mk_empty T = Const (\<^const_name>\<open>Limited_Sequence.neg_empty\<close>, mk_neg_dseqT T)
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name Limited_Sequence.neg_single}, T --> mk_neg_dseqT T) $ t end
+  in Const(\<^const_name>\<open>Limited_Sequence.neg_single\<close>, T --> mk_neg_dseqT T) $ t end
 
 fun mk_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Limited_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Limited_Sequence.neg_bind\<close>, fastype_of x --> T --> U) $ x $ f
   end
   
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Limited_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Limited_Sequence.neg_decr_bind\<close>, fastype_of x --> T --> U) $ x $ f
   end
 
-val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.neg_union}
+val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Limited_Sequence.neg_union\<close>
 
 fun mk_if cond =
-  Const (@{const_name Limited_Sequence.neg_if_seq},
+  Const (\<^const_name>\<open>Limited_Sequence.neg_if_seq\<close>,
     HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
@@ -437,12 +437,12 @@
   let
     val nT = mk_neg_dseqT HOLogic.unitT
     val pT =
-      @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
-        [@{typ unit}])
-  in Const (@{const_name Limited_Sequence.neg_not_seq}, pT --> nT) $ t end
+      \<^typ>\<open>natural\<close> --> Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>,
+        [\<^typ>\<open>unit\<close>])
+  in Const (\<^const_name>\<open>Limited_Sequence.neg_not_seq\<close>, pT --> nT) $ t end
 
 fun mk_map T1 T2 tf tp =
-  Const (@{const_name Limited_Sequence.neg_map},
+  Const (\<^const_name>\<open>Limited_Sequence.neg_map\<close>,
     (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns =
@@ -464,58 +464,58 @@
 struct
 
 fun mk_pos_random_dseqT T =
-  @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
-    @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
+  \<^typ>\<open>natural\<close> --> \<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> -->
+    \<^typ>\<open>natural\<close> --> Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>, [T])
 
 fun dest_pos_random_dseqT
-    (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
-      Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural},
-      Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
+    (Type ("fun", [\<^typ>\<open>natural\<close>, Type ("fun", [\<^typ>\<open>natural\<close>,
+      Type ("fun", [\<^typ>\<open>Random.seed\<close>, Type ("fun", [\<^typ>\<open>natural\<close>,
+      Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>, [T])])])])])) = T
   | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], [])
 
-fun mk_empty T = Const (@{const_name Random_Sequence.pos_empty}, mk_pos_random_dseqT T)
+fun mk_empty T = Const (\<^const_name>\<open>Random_Sequence.pos_empty\<close>, mk_pos_random_dseqT T)
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end
+  in Const(\<^const_name>\<open>Random_Sequence.pos_single\<close>, T --> mk_pos_random_dseqT T) $ t end
 
 fun mk_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Random_Sequence.pos_bind\<close>, fastype_of x --> T --> U) $ x $ f
   end
 
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Random_Sequence.pos_decr_bind\<close>, fastype_of x --> T --> U) $ x $ f
   end
 
-val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.pos_union};
+val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Random_Sequence.pos_union\<close>;
 
-fun mk_if cond = Const (@{const_name Random_Sequence.pos_if_random_dseq},
+fun mk_if cond = Const (\<^const_name>\<open>Random_Sequence.pos_if_random_dseq\<close>,
   HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto T (f, from, to) =
-  list_comb (Const (@{const_name Random_Sequence.pos_iterate_upto},
-      [@{typ natural} --> T, @{typ natural}, @{typ natural}]
+  list_comb (Const (\<^const_name>\<open>Random_Sequence.pos_iterate_upto\<close>,
+      [\<^typ>\<open>natural\<close> --> T, \<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>]
         ---> mk_pos_random_dseqT T),
     [f, from, to])
 
 fun mk_not t =
   let
     val pT = mk_pos_random_dseqT HOLogic.unitT
-    val nT = @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
-      @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
-        [Type (@{type_name Option.option}, [@{typ unit}])])
+    val nT = \<^typ>\<open>natural\<close> --> \<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> -->
+      \<^typ>\<open>natural\<close> --> Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>,
+        [Type (\<^type_name>\<open>Option.option\<close>, [\<^typ>\<open>unit\<close>])])
 
-  in Const (@{const_name Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
+  in Const (\<^const_name>\<open>Random_Sequence.pos_not_random_dseq\<close>, nT --> pT) $ t end
 
 fun mk_map T1 T2 tf tp =
-  Const (@{const_name Random_Sequence.pos_map},
+  Const (\<^const_name>\<open>Random_Sequence.pos_map\<close>,
     (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns =
@@ -537,59 +537,59 @@
 struct
 
 fun mk_neg_random_dseqT T =
-  @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
-    @{typ natural} --> 
-    Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
+  \<^typ>\<open>natural\<close> --> \<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> -->
+    \<^typ>\<open>natural\<close> --> 
+    Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>, [Type (\<^type_name>\<open>Option.option\<close>, [T])])
 
 fun dest_neg_random_dseqT
-    (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
-      Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural},
-        Type (@{type_name Lazy_Sequence.lazy_sequence},
-          [Type (@{type_name Option.option}, [T])])])])])])) = T
+    (Type ("fun", [\<^typ>\<open>natural\<close>, Type ("fun", [\<^typ>\<open>natural\<close>,
+      Type ("fun", [\<^typ>\<open>Random.seed\<close>, Type ("fun", [\<^typ>\<open>natural\<close>,
+        Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>,
+          [Type (\<^type_name>\<open>Option.option\<close>, [T])])])])])])) = T
   | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], [])
 
-fun mk_empty T = Const (@{const_name Random_Sequence.neg_empty}, mk_neg_random_dseqT T)
+fun mk_empty T = Const (\<^const_name>\<open>Random_Sequence.neg_empty\<close>, mk_neg_random_dseqT T)
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end
+  in Const(\<^const_name>\<open>Random_Sequence.neg_single\<close>, T --> mk_neg_random_dseqT T) $ t end
 
 fun mk_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Random_Sequence.neg_bind\<close>, fastype_of x --> T --> U) $ x $ f
   end
 
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Random_Sequence.neg_decr_bind\<close>, fastype_of x --> T --> U) $ x $ f
   end
 
-val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.neg_union}
+val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Random_Sequence.neg_union\<close>
 
 fun mk_if cond =
-  Const (@{const_name Random_Sequence.neg_if_random_dseq},
+  Const (\<^const_name>\<open>Random_Sequence.neg_if_random_dseq\<close>,
     HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto T (f, from, to) =
-  list_comb (Const (@{const_name Random_Sequence.neg_iterate_upto},
-      [@{typ natural} --> T, @{typ natural}, @{typ natural}]
+  list_comb (Const (\<^const_name>\<open>Random_Sequence.neg_iterate_upto\<close>,
+      [\<^typ>\<open>natural\<close> --> T, \<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>]
         ---> mk_neg_random_dseqT T),
     [f, from, to])
 
 fun mk_not t =
   let
     val nT = mk_neg_random_dseqT HOLogic.unitT
-    val pT = @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
-    @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}])
-  in Const (@{const_name Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
+    val pT = \<^typ>\<open>natural\<close> --> \<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> -->
+    \<^typ>\<open>natural\<close> --> Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>, [\<^typ>\<open>unit\<close>])
+  in Const (\<^const_name>\<open>Random_Sequence.neg_not_random_dseq\<close>, pT --> nT) $ t end
 
 fun mk_map T1 T2 tf tp =
-  Const (@{const_name Random_Sequence.neg_map},
+  Const (\<^const_name>\<open>Random_Sequence.neg_map\<close>,
     (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns =
@@ -611,34 +611,34 @@
 struct
 
 fun mk_random_dseqT T =
-  @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
-    HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed})
+  \<^typ>\<open>natural\<close> --> \<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> -->
+    HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, \<^typ>\<open>Random.seed\<close>)
 
 fun dest_random_dseqT
-    (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
-      Type ("fun", [@{typ Random.seed},
-      Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) =
+    (Type ("fun", [\<^typ>\<open>natural\<close>, Type ("fun", [\<^typ>\<open>natural\<close>,
+      Type ("fun", [\<^typ>\<open>Random.seed\<close>,
+      Type (\<^type_name>\<open>Product_Type.prod\<close>, [T, \<^typ>\<open>Random.seed\<close>])])])])) =
       DSequence_CompFuns.dest_dseqT T
   | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], [])
 
-fun mk_empty T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T)
+fun mk_empty T = Const (\<^const_name>\<open>Random_Sequence.empty\<close>, mk_random_dseqT T)
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end
+  in Const(\<^const_name>\<open>Random_Sequence.single\<close>, T --> mk_random_dseqT T) $ t end
 
 fun mk_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
+    Const (\<^const_name>\<open>Random_Sequence.bind\<close>, fastype_of x --> T --> U) $ x $ f
   end
 
-val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.union}
+val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Random_Sequence.union\<close>
 
 fun mk_if cond =
-  Const (@{const_name Random_Sequence.if_random_dseq},
+  Const (\<^const_name>\<open>Random_Sequence.if_random_dseq\<close>,
     HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
@@ -646,9 +646,9 @@
 fun mk_not t =
   let
     val T = mk_random_dseqT HOLogic.unitT
-  in Const (@{const_name Random_Sequence.not_random_dseq}, T --> T) $ t end
+  in Const (\<^const_name>\<open>Random_Sequence.not_random_dseq\<close>, T --> T) $ t end
 
-fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map},
+fun mk_map T1 T2 tf tp = Const (\<^const_name>\<open>Random_Sequence.map\<close>,
   (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
 
 val compfuns =