--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Fri Jan 04 23:22:53 2019 +0100
@@ -57,7 +57,7 @@
(case AList.lookup (op =) (!vars) (T, U) of
SOME V => V
| NONE =>
- let val V = TVar ((Name.aT, length (!vars) + max_j), @{sort type}) in
+ let val V = TVar ((Name.aT, length (!vars) + max_j), \<^sort>\<open>type\<close>) in
vars := ((T, U), V) :: !vars; V
end);
@@ -106,7 +106,7 @@
val num_curry_uncurryN_balanced_precomp = 8;
val curry_uncurryN_balanced_precomp =
- map (mk_curry_uncurryN_balanced_raw @{context}) (0 upto num_curry_uncurryN_balanced_precomp);
+ map (mk_curry_uncurryN_balanced_raw \<^context>) (0 upto num_curry_uncurryN_balanced_precomp);
fun mk_curry_uncurryN_balanced ctxt n =
if n <= num_curry_uncurryN_balanced_precomp then nth curry_uncurryN_balanced_precomp n