diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -89,8 +89,8 @@
   in mk_eqs x xs end;
 
 fun mk_tracing s t =
-  Const(@{const_name Code_Evaluation.tracing},
-    @{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t
+  Const(\<^const_name>\<open>Code_Evaluation.tracing\<close>,
+    \<^typ>\<open>String.literal\<close> --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t
 
 
 (* representation of inferred clauses with modes *)
@@ -202,11 +202,11 @@
   let
     fun check (Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
       | check m (Type("fun", _)) = (m = Input orelse m = Output)
-      | check (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+      | check (Pair (m1, m2)) (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) =
           check m1 T1 andalso check m2 T2
       | check Input _ = true
       | check Output _ = true
-      | check Bool @{typ bool} = true
+      | check Bool \<^typ>\<open>bool\<close> = true
       | check _ _ = false
     fun check_consistent_modes ms =
       if forall (fn Fun _ => true | _ => false) ms then
@@ -306,18 +306,18 @@
   additional_arguments = fn names =>
     let
       val depth_name = singleton (Name.variant_list names) "depth"
-    in [Free (depth_name, @{typ natural})] end,
+    in [Free (depth_name, \<^typ>\<open>natural\<close>)] end,
   modify_funT = (fn T => let val (Ts, U) = strip_type T
-  val Ts' = [@{typ natural}] in (Ts @ Ts') ---> U end),
+  val Ts' = [\<^typ>\<open>natural\<close>] in (Ts @ Ts') ---> U end),
   wrap_compilation =
     fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
     let
       val [depth] = additional_arguments
       val (_, Ts) = split_modeT mode (binder_types T)
       val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts)
-      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
+      val if_const = Const (\<^const_name>\<open>If\<close>, \<^typ>\<open>bool\<close> --> T' --> T' --> T')
     in
-      if_const $ HOLogic.mk_eq (depth, @{term "0 :: natural"})
+      if_const $ HOLogic.mk_eq (depth, \<^term>\<open>0 :: natural\<close>)
         $ mk_empty compfuns (dest_monadT compfuns T')
         $ compilation
     end,
@@ -326,8 +326,8 @@
     let
       val [depth] = additional_arguments
       val depth' =
-        Const (@{const_name Groups.minus}, @{typ "natural => natural => natural"})
-          $ depth $ Const (@{const_name Groups.one}, @{typ "natural"})
+        Const (\<^const_name>\<open>Groups.minus\<close>, \<^typ>\<open>natural => natural => natural\<close>)
+          $ depth $ Const (\<^const_name>\<open>Groups.one\<close>, \<^typ>\<open>natural\<close>)
     in [depth'] end
   }
 
@@ -337,20 +337,20 @@
   function_name_prefix = "random_",
   compfuns = Predicate_Comp_Funs.compfuns,
   mk_random = (fn T => fn additional_arguments =>
-  list_comb (Const(@{const_name Random_Pred.iter},
-  [@{typ natural}, @{typ natural}, @{typ Random.seed}] --->
+  list_comb (Const(\<^const_name>\<open>Random_Pred.iter\<close>,
+  [\<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>, \<^typ>\<open>Random.seed\<close>] --->
     Predicate_Comp_Funs.mk_monadT T), additional_arguments)),
   modify_funT = (fn T =>
     let
       val (Ts, U) = strip_type T
-      val Ts' = [@{typ natural}, @{typ natural}, @{typ Random.seed}]
+      val Ts' = [\<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>, \<^typ>\<open>Random.seed\<close>]
     in (Ts @ Ts') ---> U end),
   additional_arguments = (fn names =>
     let
       val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
     in
-      [Free (nrandom, @{typ natural}), Free (size, @{typ natural}),
-        Free (seed, @{typ Random.seed})]
+      [Free (nrandom, \<^typ>\<open>natural\<close>), Free (size, \<^typ>\<open>natural\<close>),
+        Free (seed, \<^typ>\<open>Random.seed\<close>)]
     end),
   wrap_compilation = K (K (K (K (K I))))
     : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
@@ -363,21 +363,21 @@
   function_name_prefix = "depth_limited_random_",
   compfuns = Predicate_Comp_Funs.compfuns,
   mk_random = (fn T => fn additional_arguments =>
-  list_comb (Const(@{const_name Random_Pred.iter},
-  [@{typ natural}, @{typ natural}, @{typ Random.seed}] --->
+  list_comb (Const(\<^const_name>\<open>Random_Pred.iter\<close>,
+  [\<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>, \<^typ>\<open>Random.seed\<close>] --->
     Predicate_Comp_Funs.mk_monadT T), tl additional_arguments)),
   modify_funT = (fn T =>
     let
       val (Ts, U) = strip_type T
-      val Ts' = [@{typ natural}, @{typ natural}, @{typ natural},
-        @{typ Random.seed}]
+      val Ts' = [\<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>,
+        \<^typ>\<open>Random.seed\<close>]
     in (Ts @ Ts') ---> U end),
   additional_arguments = (fn names =>
     let
       val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
     in
-      [Free (depth, @{typ natural}), Free (nrandom, @{typ natural}),
-        Free (size, @{typ natural}), Free (seed, @{typ Random.seed})]
+      [Free (depth, \<^typ>\<open>natural\<close>), Free (nrandom, \<^typ>\<open>natural\<close>),
+        Free (size, \<^typ>\<open>natural\<close>), Free (seed, \<^typ>\<open>Random.seed\<close>)]
     end),
   wrap_compilation =
   fn compfuns => fn _ => fn T => fn mode => fn additional_arguments => fn compilation =>
@@ -386,9 +386,9 @@
       val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE))
         mode (binder_types T)
       val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts)
-      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
+      val if_const = Const (\<^const_name>\<open>If\<close>, \<^typ>\<open>bool\<close> --> T' --> T' --> T')
     in
-      if_const $ HOLogic.mk_eq (depth, @{term "0 :: natural"})
+      if_const $ HOLogic.mk_eq (depth, \<^term>\<open>0 :: natural\<close>)
         $ mk_empty compfuns (dest_monadT compfuns T')
         $ compilation
     end,
@@ -397,8 +397,8 @@
     let
       val [depth, nrandom, size, seed] = additional_arguments
       val depth' =
-        Const (@{const_name Groups.minus}, @{typ "natural => natural => natural"})
-          $ depth $ Const (@{const_name Groups.one}, @{typ "natural"})
+        Const (\<^const_name>\<open>Groups.minus\<close>, \<^typ>\<open>natural => natural => natural\<close>)
+          $ depth $ Const (\<^const_name>\<open>Groups.one\<close>, \<^typ>\<open>natural\<close>)
     in [depth', nrandom, size, seed] end
 }
 
@@ -435,12 +435,12 @@
   compfuns = Random_Sequence_CompFuns.compfuns,
   mk_random = (fn T => fn _ =>
   let
-    val random = Const (@{const_name Quickcheck_Random.random},
-      @{typ natural} --> @{typ Random.seed} -->
-        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
+    val random = Const (\<^const_name>\<open>Quickcheck_Random.random\<close>,
+      \<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> -->
+        HOLogic.mk_prodT (HOLogic.mk_prodT (T, \<^typ>\<open>unit => term\<close>), \<^typ>\<open>Random.seed\<close>))
   in
-    Const (@{const_name Random_Sequence.Random}, (@{typ natural} --> @{typ Random.seed} -->
-      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
+    Const (\<^const_name>\<open>Random_Sequence.Random\<close>, (\<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> -->
+      HOLogic.mk_prodT (HOLogic.mk_prodT (T, \<^typ>\<open>unit => term\<close>), \<^typ>\<open>Random.seed\<close>)) -->
       Random_Sequence_CompFuns.mk_random_dseqT T) $ random
   end),
 
@@ -472,12 +472,12 @@
   compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns,
   mk_random = (fn T => fn _ =>
   let
-    val random = Const (@{const_name Quickcheck_Random.random},
-      @{typ natural} --> @{typ Random.seed} -->
-        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
+    val random = Const (\<^const_name>\<open>Quickcheck_Random.random\<close>,
+      \<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> -->
+        HOLogic.mk_prodT (HOLogic.mk_prodT (T, \<^typ>\<open>unit => term\<close>), \<^typ>\<open>Random.seed\<close>))
   in
-    Const (@{const_name Random_Sequence.pos_Random}, (@{typ natural} --> @{typ Random.seed} -->
-      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
+    Const (\<^const_name>\<open>Random_Sequence.pos_Random\<close>, (\<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> -->
+      HOLogic.mk_prodT (HOLogic.mk_prodT (T, \<^typ>\<open>unit => term\<close>), \<^typ>\<open>Random.seed\<close>)) -->
       New_Pos_Random_Sequence_CompFuns.mk_pos_random_dseqT T) $ random
   end),
   modify_funT = I,
@@ -507,8 +507,8 @@
   compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns,
   mk_random =
     (fn T => fn _ =>
-      Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"},
-        @{typ "natural"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T]))),
+      Const (\<^const_name>\<open>Lazy_Sequence.small_lazy_class.small_lazy\<close>,
+        \<^typ>\<open>natural\<close> --> Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>, [T]))),
   modify_funT = I,
   additional_arguments = K [],
   wrap_compilation = K (K (K (K (K I))))
@@ -536,9 +536,9 @@
   compfuns = Pos_Bounded_CPS_Comp_Funs.compfuns,
   mk_random =
     (fn T => fn _ =>
-       Const (@{const_name "Quickcheck_Exhaustive.exhaustive"},
-       (T --> @{typ "(bool * term list) option"}) -->
-         @{typ "natural => (bool * term list) option"})),
+       Const (\<^const_name>\<open>Quickcheck_Exhaustive.exhaustive\<close>,
+       (T --> \<^typ>\<open>(bool * term list) option\<close>) -->
+         \<^typ>\<open>natural => (bool * term list) option\<close>)),
   modify_funT = I,
   additional_arguments = K [],
   wrap_compilation = K (K (K (K (K I))))
@@ -597,7 +597,7 @@
 (** specific rpred functions -- move them to the correct place in this file *)
 fun mk_Eval_of (P as (Free _), T) mode =
   let
-    fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
+    fun mk_bounds (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) i =
           let
             val (bs2, i') = mk_bounds T2 i
             val (bs1, i'') = mk_bounds T1 i'
@@ -608,9 +608,9 @@
     fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2))
     fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT)
       | mk_tuple tTs = foldr1 mk_prod tTs
-    fun mk_split_abs (T as Type (@{type_name Product_Type.prod}, [T1, T2])) t =
+    fun mk_split_abs (T as Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) t =
           absdummy T
-            (HOLogic.case_prod_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
+            (HOLogic.case_prod_const (T1, T2, \<^typ>\<open>bool\<close>) $ (mk_split_abs T1 (mk_split_abs T2 t)))
       | mk_split_abs T t = absdummy T t
     val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
     val (inargs, outargs) = split_mode mode args
@@ -655,7 +655,7 @@
     lambda v (Case_Translation.make_case ctxt Case_Translation.Quiet Name.context v
       [(HOLogic.mk_tuple out_ts,
         if null eqs'' then success_t
-        else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
+        else Const (\<^const_name>\<open>HOL.If\<close>, HOLogic.boolT --> U --> U --> U) $
           foldr1 HOLogic.mk_conj eqs'' $ success_t $
             mk_empty compfuns U'),
        (v', mk_empty compfuns U')])
@@ -689,7 +689,7 @@
             val bs = map (pair "x") (binder_types (fastype_of t))
             val bounds = map Bound (rev (0 upto (length bs) - 1))
           in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end
-      | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
+      | (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
           (case (expr_of (t1, d1), expr_of (t2, d2)) of
             (NONE, NONE) => NONE
           | (NONE, SOME t) => SOME t
@@ -820,8 +820,8 @@
   argument_position_pair (nth (strip_fun_mode mode) i) is)
 
 fun nth_pair [] t = t
-  | nth_pair (1 :: is) (Const (@{const_name Pair}, _) $ t1 $ _) = nth_pair is t1
-  | nth_pair (2 :: is) (Const (@{const_name Pair}, _) $ _ $ t2) = nth_pair is t2
+  | nth_pair (1 :: is) (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ _) = nth_pair is t1
+  | nth_pair (2 :: is) (Const (\<^const_name>\<open>Pair\<close>, _) $ _ $ t2) = nth_pair is t2
   | nth_pair _ _ = raise Fail "unexpected input for nth_tuple"
 
 
@@ -1023,11 +1023,11 @@
 
 (* Definition of executable functions and their intro and elim rules *)
 
-fun strip_split_abs (Const (@{const_name case_prod}, _) $ t) = strip_split_abs t
+fun strip_split_abs (Const (\<^const_name>\<open>case_prod\<close>, _) $ t) = strip_split_abs t
   | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
   | strip_split_abs t = t
 
-fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names =
+fun mk_args is_eval (m as Pair (m1, m2), T as Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) names =
       if eq_mode (m, Input) orelse eq_mode (m, Output) then
         let
           val x = singleton (Name.variant_list names) "x"
@@ -1213,7 +1213,7 @@
 fun dest_prem ctxt params t =
   (case strip_comb t of
     (v as Free _, _) => if member (op =) params v then Prem t else Sidecond t
-  | (c as Const (@{const_name Not}, _), [t]) =>
+  | (c as Const (\<^const_name>\<open>Not\<close>, _), [t]) =>
       (case dest_prem ctxt params t of
         Prem t => Negprem t
       | Negprem _ => error ("Double negation not allowed in premise: " ^
@@ -1341,8 +1341,8 @@
               (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
             val args = map2 (curry Free) arg_names Ts
             val predfun = Const (Core_Data.function_name_of Pred ctxt predname full_mode,
-              Ts ---> Predicate_Comp_Funs.mk_monadT @{typ unit})
-            val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
+              Ts ---> Predicate_Comp_Funs.mk_monadT \<^typ>\<open>unit\<close>)
+            val rhs = \<^term>\<open>Predicate.holds\<close> $ (list_comb (predfun, args))
             val eq_term = HOLogic.mk_Trueprop
               (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
             val def = Core_Data.predfun_definition_of ctxt predname full_mode
@@ -1610,12 +1610,12 @@
 (* values_timeout configuration *)
 
 val values_timeout =
-  Attrib.setup_config_real @{binding values_timeout} (K 40.0)
+  Attrib.setup_config_real \<^binding>\<open>values_timeout\<close> (K 40.0)
 
 val _ =
   Theory.setup
    (Core_Data.PredData.put (Graph.empty) #>
-    Attrib.setup @{binding code_pred_intro}
+    Attrib.setup \<^binding>\<open>code_pred_intro\<close>
       (Scan.lift (Scan.option Args.name) >> attrib' Core_Data.add_intro)
       "adding alternative introduction rules for code generation of inductive predicates")
 
@@ -1723,7 +1723,7 @@
   let
     val (inner_t, T_compr) =
       (case t of
-        (Const (@{const_name Collect}, _) $ Abs (_, T, t)) => (t, T)
+        (Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, T, t)) => (t, T)
       | _ => raise TERM ("dest_special_compr", [t]))
     val (Ts, conj) = apfst (map snd) (Predicate_Compile_Aux.strip_ex inner_t)
     val [eq, body] = HOLogic.dest_conj conj
@@ -1744,7 +1744,7 @@
   let
     val inner_t =
       (case t_compr of
-        (Const (@{const_name Collect}, _) $ t) => t
+        (Const (\<^const_name>\<open>Collect\<close>, _) $ t) => t
       | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr))
     val (body, Ts, fp) = HOLogic.strip_ptupleabs inner_t;
     val output_names = Name.variant_list (Term.add_free_names body [])
@@ -1774,7 +1774,7 @@
   in
     if Core_Data.defined_functions compilation ctxt name then
       let
-        fun extract_mode (Const (@{const_name Pair}, _) $ t1 $ t2) =
+        fun extract_mode (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2) =
               Pair (extract_mode t1, extract_mode t2)
           | extract_mode (Free (x, _)) =
               if member (op =) output_names x then Output else Input
@@ -1857,13 +1857,13 @@
       (case compilation of
         Pred => []
       | Random =>
-          map (HOLogic.mk_number @{typ "natural"}) arguments @
-            [@{term "(1, 1) :: natural * natural"}]
+          map (HOLogic.mk_number \<^typ>\<open>natural\<close>) arguments @
+            [\<^term>\<open>(1, 1) :: natural * natural\<close>]
       | Annotated => []
-      | Depth_Limited => [HOLogic.mk_number @{typ "natural"} (hd arguments)]
+      | Depth_Limited => [HOLogic.mk_number \<^typ>\<open>natural\<close> (hd arguments)]
       | Depth_Limited_Random =>
-          map (HOLogic.mk_number @{typ "natural"}) arguments @
-            [@{term "(1, 1) :: natural * natural"}]
+          map (HOLogic.mk_number \<^typ>\<open>natural\<close>) arguments @
+            [\<^term>\<open>(1, 1) :: natural * natural\<close>]
       | DSeq => []
       | Pos_Random_DSeq => []
       | New_Pos_Random_DSeq => []
@@ -1873,9 +1873,9 @@
     val T = dest_monadT compfuns (fastype_of t)
     val t' =
       if stats andalso compilation = New_Pos_Random_DSeq then
-        mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ natural}))
+        mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, \<^typ>\<open>natural\<close>))
           (absdummy T (HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0,
-            @{term natural_of_nat} $ (HOLogic.size_const T $ Bound 0)))) t
+            \<^term>\<open>natural_of_nat\<close> $ (HOLogic.size_const T $ Bound 0)))) t
       else
         mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
     val time_limit = seconds (Config.get ctxt values_timeout)
@@ -1962,7 +1962,7 @@
     val ([dots], ctxt') = ctxt
       |> Proof_Context.add_fixes [(Binding.name "dots", SOME setT, Mixfix.mixfix "...")]
     (* check expected values *)
-    val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
+    val union = Const (\<^const_abbrev>\<open>Set.union\<close>, setT --> setT --> setT)
     val () =
       (case raw_expected of
         NONE => ()