src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML

--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -201,7 +201,7 @@
   end;
 
 fun check_top_sort ctxt b T =
-  ignore (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort type}) orelse
+  ignore (Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\<open>type\<close>) orelse
     error ("Type of " ^ Binding.print b ^ " contains top sort"));
 
 datatype fp_kind = Least_FP | Greatest_FP;
@@ -264,7 +264,7 @@
 
 val mk_common_name = space_implode "_";
 
-fun num_binder_types (Type (@{type_name fun}, [_, T])) = 1 + num_binder_types T
+fun num_binder_types (Type (\<^type_name>\<open>fun\<close>, [_, T])) = 1 + num_binder_types T
   | num_binder_types _ = 0;
 
 val exists_subtype_in = Term.exists_subtype o member (op =);
@@ -278,8 +278,8 @@
   | retype_const_or_free _ t = raise TERM ("retype_const_or_free", [t]);
 
 fun drop_all t =
-  subst_bounds (strip_qnt_vars @{const_name Pure.all} t |> map Free |> rev,
-    strip_qnt_body @{const_name Pure.all} t);
+  subst_bounds (strip_qnt_vars \<^const_name>\<open>Pure.all\<close> t |> map Free |> rev,
+    strip_qnt_body \<^const_name>\<open>Pure.all\<close> t);
 
 fun permute_args n t =
   list_comb (t, map Bound (0 :: (n downto 1))) |> fold (K (Term.abs (Name.uu, dummyT))) (0 upto n);