--- a/src/HOL/Tools/Nunchaku/nunchaku_util.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_util.ML Fri Jan 04 23:22:53 2019 +0100
@@ -61,8 +61,8 @@
(* Clone from "HOL/Tools/inductive_realizer.ML". *)
val attach_typeS =
map_types (map_atyps
- (fn TFree (s, []) => TFree (s, @{sort type})
- | TVar (ixn, []) => TVar (ixn, @{sort type})
+ (fn TFree (s, []) => TFree (s, \<^sort>\<open>type\<close>)
+ | TVar (ixn, []) => TVar (ixn, \<^sort>\<open>type\<close>)
| T => T));
val specialize_type = ATP_Util.specialize_type;