--- 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
--- 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
--- 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 ..
--- 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;