--- a/src/HOL/Decision_Procs/langford_data.ML Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Decision_Procs/langford_data.ML Sat Jan 05 17:24:33 2019 +0100
@@ -90,7 +90,7 @@
val _ =
Theory.setup
- (Attrib.setup @{binding langford}
+ (Attrib.setup \<^binding>\<open>langford\<close>
((keyword qeN |-- thms) --
(keyword gatherN |-- thms) --
(keyword atomsN |-- terms) >> (fn ((qes, gs), atoms) =>
@@ -108,6 +108,6 @@
val _ =
Theory.setup
- (Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset");
+ (Attrib.setup \<^binding>\<open>langfordsimp\<close> (Attrib.add_del add_simp del_simp) "Langford simpset");
end;