# HG changeset patch # User berghofe # Date 937821701 -7200 # Node ID dee529666dcd97189a3da7b0b55c868f503e7ad9 # Parent abefbd41bd3e6dc7ce9a80068fe3c05f02110977 Fixed bug in add_primrec which caused non-informative error message. diff -r abefbd41bd3e -r dee529666dcd src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Mon Sep 20 10:46:16 1999 +0200 +++ b/src/HOL/Tools/primrec_package.ML Mon Sep 20 12:01:41 1999 +0200 @@ -24,7 +24,7 @@ fun primrec_err s = error ("Primrec definition error:\n" ^ s); fun primrec_eq_err sign s eq = - primrec_err (s ^ "\nin equation\n" ^ quote (Sign.string_of_term sign eq)); + primrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term sign eq)); (* messages *) @@ -259,11 +259,12 @@ fun add_primrec alt_name eqns thy = let + 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 (readtm (Theory.sign_of thy) propT) strings; + val eqn_ts = map (readtm sign propT) strings; val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq))) - handle TERM _ => raise RecError "not a proper equation") eqn_ts; + 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 in add_primrec_i alt_name (names ~~ eqn_ts' ~~ atts) thy