# 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