--- a/src/HOL/Tools/functor.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/functor.ML Fri Jan 04 23:22:53 2019 +0100
@@ -82,7 +82,7 @@
(* mapper properties *)
val compositionality_ss =
- simpset_of (put_simpset HOL_basic_ss @{context} addsimps [Simpdata.mk_eq @{thm comp_def}]);
+ simpset_of (put_simpset HOL_basic_ss \<^context> addsimps [Simpdata.mk_eq @{thm comp_def}]);
fun make_comp_prop ctxt variances (tyco, mapper) =
let
@@ -136,7 +136,7 @@
in (comp_prop, prove_compositionality) end;
val identity_ss =
- simpset_of (put_simpset HOL_basic_ss @{context} addsimps [Simpdata.mk_eq @{thm id_def}]);
+ simpset_of (put_simpset HOL_basic_ss \<^context> addsimps [Simpdata.mk_eq @{thm id_def}]);
fun make_id_prop ctxt variances (tyco, mapper) =
let