| 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)));