merged

--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Nov 15 14:59:53 2010 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Nov 15 17:04:53 2010 +0100
@@ -244,6 +244,10 @@
     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"