src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy
changeset 69597 ff784d5a5bfb
parent 63731 9f906a2eb0e7
child 80634 a90ab1ea6458
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -7,7 +7,7 @@
   open BNF_FP_Def_Sugar
   open BNF_LFP_Compat
 
-  val compat_plugin = Plugin_Name.declare_setup @{binding compat};
+  val compat_plugin = Plugin_Name.declare_setup \<^binding>\<open>compat\<close>;
 
   fun compat fp_sugars =
     perhaps (try (datatype_compat (map (fst o dest_Type o #T) fp_sugars)));