--- a/src/HOL/Library/Code_Char.thy Tue Sep 16 16:13:06 2008 +0200
+++ b/src/HOL/Library/Code_Char.thy Tue Sep 16 16:13:09 2008 +0200
@@ -9,8 +9,6 @@
imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
begin
-declare char.recs [code func del] char.cases [code func del]
-
code_type char
(SML "char")
(OCaml "char")
@@ -35,9 +33,6 @@
(OCaml "!((_ : char) = _)")
(Haskell infixl 4 "==")
-lemma [code func, code func del]:
- "(Code_Eval.term_of :: char \<Rightarrow> term) = Code_Eval.term_of" ..
-
code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"
(SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")