| changeset 68028 | 1f9f973eed2a |
| parent 67399 | eab6ce8368fa |
| child 69593 | 3dda49e08b9d |
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Apr 24 14:17:57 2018 +0000 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Apr 24 14:17:58 2018 +0000 @@ -244,7 +244,7 @@ section \<open>Setup for String.literal\<close> -setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name "STR"}]\<close> +setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name String.Literal}]\<close> section \<open>Simplification rules for optimisation\<close>