# HG changeset patch
# User wenzelm
# Date 1322496380 -3600
# Node ID 1d168d6c55c2f7bd7f73a82c4ef75f7e867ddc0e
# Parent  09539cdffcd7aed65a103c11f94d23ba56d45d73
tuned messages;

diff -r 09539cdffcd7 -r 1d168d6c55c2 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Mon Nov 28 17:05:41 2011 +0100
+++ b/src/HOL/Statespace/state_space.ML	Mon Nov 28 17:06:20 2011 +0100
@@ -564,7 +564,7 @@
           (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
              []  => []
            | [_] => []
-           | rs  => ["Different types for component " ^ n ^": " ^
+           | rs  => ["Different types for component " ^ quote n ^ ": " ^
                 commas (map (Syntax.string_of_typ ctxt o snd) rs)])
 
     val err_dup_types = maps check_type (duplicates fst_eq raw_parent_comps)
@@ -573,7 +573,7 @@
     val all_comps = parent_comps @ comps';
     val err_comp_in_parent = (case duplicates (op =) (map fst all_comps) of
                [] => []
-             | xs => ["Components already defined in parents: " ^ commas xs]);
+             | xs => ["Components already defined in parents: " ^ commas_quote xs]);
     val errs = err_dup_args @ err_dup_components @ err_extra_frees @
                err_dup_types @ err_comp_in_parent;
   in if null errs
@@ -611,7 +611,7 @@
       if get_silent (Context.Proof ctxt)
       then Syntax.const @{const_name StateFun.lookup} $
         Syntax.const @{const_syntax undefined} $ Syntax.free n $ s
-      else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined", []));
+      else raise TERM ("StateSpace.gen_lookup_tr: component " ^ quote n ^ " not defined", []));
 
 fun lookup_tr ctxt [s, x] =
   (case Term_Position.strip_positions x of