# 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