# HG changeset patch
# User bulwahn
# Date 1289824812 -3600
# Node ID 54eb5fd36e5e03af03dd1a04ef7f4b0e26a9aeca
# Parent  293f9f211be0268bf8918f573984030ba18e612f
ignoring the constant STR in the predicate compiler

diff -r 293f9f211be0 -r 54eb5fd36e5e src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Nov 15 00:20:36 2010 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Nov 15 13:40:12 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"