Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Improved error handling: add_primrec now prints out ill-formed equation
authorberghofe
Tue, 18 Nov 2003 09:45:45 +0100
changeset 14258 9bd184c007f0
parent 14257 a7ef3f7588c5
child 14259 79f7d3451b1e
Improved error handling: add_primrec now prints out ill-formed equation in case of parse errors.
src/HOL/Tools/primrec_package.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle