--- a/src/ZF/equalities.thy Fri Jan 04 21:49:06 2019 +0100
+++ b/src/ZF/equalities.thy Fri Jan 04 23:22:53 2019 +0100
@@ -68,7 +68,7 @@
by blast
-subsection\<open>Finite Set Constructions Using @{term cons}\<close>
+subsection\<open>Finite Set Constructions Using \<^term>\<open>cons\<close>\<close>
lemma cons_subsetI: "[| a\<in>C; B\<subseteq>C |] ==> cons(a,B) \<subseteq> C"
by blast
@@ -971,13 +971,13 @@
ML \<open>
val subset_cs =
- claset_of (@{context}
+ claset_of (\<^context>
delrules [@{thm subsetI}, @{thm subsetCE}]
addSIs @{thms subset_SIs}
addIs [@{thm Union_upper}, @{thm Inter_lower}]
addSEs [@{thm cons_subsetE}]);
-val ZF_cs = claset_of (@{context} delrules [@{thm equalityI}]);
+val ZF_cs = claset_of (\<^context> delrules [@{thm equalityI}]);
\<close>
end