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