# HG changeset patch
# User bulwahn
# Date 1319006249 -7200
# Node ID 10202ca034b00cb14586e095ddbc5831cacf369f
# Parent  c8eb935e2e875062cd8f8c474c58805ad8a065fe
removing old code generator setup for strings

diff -r c8eb935e2e87 -r 10202ca034b0 src/HOL/String.thy
--- a/src/HOL/String.thy	Wed Oct 19 08:37:27 2011 +0200
+++ b/src/HOL/String.thy	Wed Oct 19 08:37:29 2011 +0200
@@ -213,31 +213,6 @@
   (Haskell infix 4 "==")
   (Scala infixl 5 "==")
 
-types_code
-  "char" ("string")
-attach (term_of) {*
-val term_of_char = HOLogic.mk_char o ord;
-*}
-attach (test) {*
-fun gen_char i =
-  let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
-  in (chr j, fn () => HOLogic.mk_char j) end;
-*}
-
-setup {*
-let
-
-fun char_codegen thy mode defs dep thyname b t gr =
-  let
-    val i = HOLogic.dest_char t;
-    val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false
-      (fastype_of t) gr;
-  in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
-  end handle TERM _ => NONE;
-
-in Codegen.add_codegen "char_codegen" char_codegen end
-*}
-
 hide_type (open) literal
 
 end