# HG changeset patch
# User Andreas Lochbihler
# Date 1392191798 -3600
# Node ID 90f2ceed2828f45ff46ef2315f94f622972a3c38
# Parent  eae296b5ef3305ebc1bcc0592584a060eb644715
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals

diff -r eae296b5ef33 -r 90f2ceed2828 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Tue Feb 11 12:08:44 2014 +0100
+++ b/src/HOL/Library/Char_ord.thy	Wed Feb 12 08:56:38 2014 +0100
@@ -97,6 +97,7 @@
 instantiation String.literal :: linorder
 begin
 
+context includes literal.lifting begin
 lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
 lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
 
@@ -109,6 +110,7 @@
 qed
 
 end
+end
 
 lemma less_literal_code [code]: 
   "op < = (\<lambda>xs ys. ord.lexordp op < (explode xs) (explode ys))"
@@ -118,6 +120,9 @@
   "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (explode xs) (explode ys))"
 by(simp add: less_eq_literal.rep_eq fun_eq_iff)
 
+lifting_update literal.lifting
+lifting_forget literal.lifting
+
 text {* Legacy aliasses *}
 
 lemmas nibble_less_eq_def = less_eq_nibble_def
diff -r eae296b5ef33 -r 90f2ceed2828 src/HOL/String.thy
--- a/src/HOL/String.thy	Tue Feb 11 12:08:44 2014 +0100
+++ b/src/HOL/String.thy	Wed Feb 12 08:56:38 2014 +0100
@@ -391,6 +391,9 @@
   "STR xs = STR ys \<longleftrightarrow> xs = ys"
   by (simp add: STR_inject)
 
+lifting_update literal.lifting
+lifting_forget literal.lifting
+
 subsection {* Code generator *}
 
 ML_file "Tools/string_code.ML"