adding another String.literal example

--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Fri Sep 10 10:59:09 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Fri Sep 10 10:59:10 2010 +0200
@@ -1501,6 +1501,27 @@
 
 thm is_error.equation
 
+inductive is_error' :: "String.literal \<Rightarrow> bool"
+where
+  "is_error' (STR ''Error1'')"
+| "is_error' (STR ''Error2'')"
+
+code_pred is_error' .
+
+thm is_error'.equation
+
+datatype ErrorObject = Error String.literal int
+
+inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
+where
+  "is_error'' (Error Error_1 3)"
+| "is_error'' (Error Error_2 4)"
+
+code_pred is_error'' .
+
+thm is_error''.equation
+
+
 section {* Examples for detecting switches *}
 
 inductive detect_switches1 where