--- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Sat Jan 05 17:24:33 2019 +0100
@@ -103,7 +103,7 @@
(* axiomatize type constructor arities *)
fun thy_arity (_, _, (lhsT, _)) =
let val (dname, tvars) = dest_Type lhsT
- in (dname, map (snd o dest_TFree) tvars, @{sort pcpo}) end
+ in (dname, map (snd o dest_TFree) tvars, \<^sort>\<open>pcpo\<close>) end
val thy = fold (Axclass.arity_axiomatization o thy_arity) dom_eqns thy
(* declare and axiomatize abs/rep *)