# HG changeset patch # User berghofe # Date 1069145145 -3600 # Node ID 9bd184c007f00055965b75f441222e142d90af7d # Parent a7ef3f7588c5aa79828b6442793098ec980da7c6 Improved error handling: add_primrec now prints out ill-formed equation in case of parse errors. diff -r a7ef3f7588c5 -r 9bd184c007f0 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Fri Nov 14 14:35:55 2003 +0100 +++ b/src/HOL/Tools/primrec_package.ML Tue Nov 18 09:45:45 2003 +0100 @@ -273,7 +273,8 @@ val sign = Theory.sign_of thy; val ((names, strings), srcss) = apfst split_list (split_list eqns); val atts = map (map (Attrib.global_attribute thy)) srcss; - val eqn_ts = map (term_of o Thm.read_cterm sign o rpair propT) strings; + val eqn_ts = map (fn s => term_of (Thm.read_cterm sign (s, propT)) + handle ERROR => error ("The error(s) above occurred for " ^ s)) strings; val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq))) handle TERM _ => primrec_eq_err sign "not a proper equation" eq) eqn_ts; val (_, eqn_ts') = InductivePackage.unify_consts (sign_of thy) rec_ts eqn_ts