src/HOL/Library/Predicate_Compile_Alternative_Defs.thy

     apply auto
     apply fastsimp
     done
 qed
 
+section {* Setup for String.literal *}
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name "STR"}] *}
+
 section {* Simplification rules for optimisation *}
 
 lemma [code_pred_simp]: "\<not> False == True"
 by auto