# HG changeset patch
# User bulwahn
# Date 1284109149 -7200
# Node ID b17ffa9652234bee2c3a89e2c739cc702d496ec0
# Parent  92aa2a0f7399bb93c70abd2c7f4996070c830b3c
fiddling with the correct setup for String.literal

diff -r 92aa2a0f7399 -r b17ffa965223 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Fri Sep 10 10:59:07 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Fri Sep 10 10:59:09 2010 +0200
@@ -159,6 +159,18 @@
 *}
 
 
+instantiation String.literal :: term_of
+begin
+
+definition
+  "term_of s = App (Const (STR ''STR'')
+    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
+      Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
+
+instance ..
+
+end
+
 subsubsection {* Code generator setup *}
 
 lemmas [code del] = term.recs term.cases term.size
diff -r 92aa2a0f7399 -r b17ffa965223 src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Sep 10 10:59:07 2010 +0200
+++ b/src/HOL/String.thy	Fri Sep 10 10:59:09 2010 +0200
@@ -157,8 +157,6 @@
 typedef (open) literal = "UNIV :: string \<Rightarrow> bool"
   morphisms explode STR ..
 
-code_datatype STR
-
 instantiation literal :: size
 begin
 
@@ -183,6 +181,10 @@
 
 end
 
+lemma STR_inject' [simp]: "(STR xs = STR ys) = (xs = ys)"
+by(simp add: STR_inject)
+
+
 subsection {* Code generator *}
 
 use "Tools/string_code.ML"