# HG changeset patch
# User haftmann
# Date 1250263654 -7200
# Node ID d33f5a96df0bc717fd99eb5aec9f183a8ad34305
# Parent  e71186d61172be8e795c15c5294e188615a1cdba# Parent  62617ef2c0d0dee0153871c25c6220dcb2e431b6
merged

diff -r e71186d61172 -r d33f5a96df0b src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Fri Aug 14 13:45:52 2009 +0100
+++ b/src/HOL/Code_Eval.thy	Fri Aug 14 17:27:34 2009 +0200
@@ -134,7 +134,7 @@
 
 lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
     (let (n, m) = nibble_pair_of_char c
-  in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
+  in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
     (Code_Eval.term_of n)) (Code_Eval.term_of m))"
   by (subst term_of_anything) rule 
 
diff -r e71186d61172 -r d33f5a96df0b src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Fri Aug 14 13:45:52 2009 +0100
+++ b/src/HOL/Predicate.thy	Fri Aug 14 17:27:34 2009 +0200
@@ -646,7 +646,7 @@
 @{code_datatype pred = Seq};
 @{code_datatype seq = Empty | Insert | Join};
 
-fun yield (Seq f) = next (f ())
+fun yield (@{code Seq} f) = next (f ())
 and next @{code Empty} = NONE
   | next (@{code Insert} (x, P)) = SOME (x, P)
   | next (@{code Join} (P, xq)) = (case yield P
diff -r e71186d61172 -r d33f5a96df0b src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Fri Aug 14 13:45:52 2009 +0100
+++ b/src/HOL/Quickcheck.thy	Fri Aug 14 17:27:34 2009 +0200
@@ -54,7 +54,7 @@
 begin
 
 definition 
-  "random _ = Pair (STR [], \<lambda>u. Code_Eval.term_of (STR []))"
+  "random _ = Pair (STR '''', \<lambda>u. Code_Eval.term_of (STR ''''))"
 
 instance ..
 
diff -r e71186d61172 -r d33f5a96df0b src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Aug 14 13:45:52 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Aug 14 17:27:34 2009 +0200
@@ -119,7 +119,7 @@
     val tycos = map fst dataTs;
     val _ = if gen_eq_set (op =) (tycos, raw_tycos) then ()
       else error ("Type constructors " ^ commas (map quote raw_tycos)
-        ^ "do not belong exhaustively to one mutual recursive datatype");
+        ^ " do not belong exhaustively to one mutual recursive datatype");
 
     val (Ts, Us) = (pairself o map) Type protoTs;