# HG changeset patch
# User bulwahn
# Date 1305726333 -7200
# Node ID 6ef538f6a8abb0d365827f97facdfec4f155ec2a
# Parent  9079f49053e5ed7c7ffa059b8eb33c9a34859ef7
adding Code_Char_ord to code generation regression tests

diff -r 9079f49053e5 -r 6ef538f6a8ab src/HOL/Codegenerator_Test/Candidates_Pretty.thy
--- a/src/HOL/Codegenerator_Test/Candidates_Pretty.thy	Wed May 18 15:45:33 2011 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates_Pretty.thy	Wed May 18 15:45:33 2011 +0200
@@ -4,7 +4,7 @@
 header {* Generating code using pretty literals and natural number literals  *}
 
 theory Candidates_Pretty
-imports Candidates Code_Char Efficient_Nat
+imports Candidates Code_Char_ord Efficient_Nat
 begin
 
 end
diff -r 9079f49053e5 -r 6ef538f6a8ab src/HOL/Codegenerator_Test/Generate_Pretty.thy
--- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Wed May 18 15:45:33 2011 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Wed May 18 15:45:33 2011 +0200
@@ -9,8 +9,6 @@
 
 lemma [code, code del]: "nat_of_char = nat_of_char" ..
 lemma [code, code del]: "char_of_nat = char_of_nat" ..
-lemma [code, code del]: "(less_eq :: char \<Rightarrow> _) = less_eq" ..
-lemma [code, code del]: "(less :: char \<Rightarrow> _) = less" ..
 
 subsection {* Check whether generated code compiles *}