src/HOL/Tools/Transfer/transfer_bnf.ML
changeset 69593 3dda49e08b9d
parent 67703 8c4806fe827f
child 70316 c61b7af108a6
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -33,7 +33,7 @@
     val PT = fastype_of P
     val argT = hd (binder_types PT)
   in
-    Const (@{const_name Domainp}, PT --> argT --> HOLogic.boolT) $ P
+    Const (\<^const_name>\<open>Domainp\<close>, PT --> argT --> HOLogic.boolT) $ P
   end
 
 fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst