# HG changeset patch
# User paulson
# Date 953304590 -3600
# Node ID 6343c725ba7e05b8d10558ce779d9a974e68adf7
# Parent  82826ed95d4ba13837491bff08ac7b93f1706d27
better error messages, especially for multiple types

diff -r 82826ed95d4b -r 6343c725ba7e TFL/tfl.sml
--- a/TFL/tfl.sml	Thu Mar 16 00:36:22 2000 +0100
+++ b/TFL/tfl.sml	Fri Mar 17 15:49:50 2000 +0100
@@ -302,13 +302,20 @@
   | dest_atom  _ = raise TFL_ERR {func="dest_atom", 
 				  mesg="function name not an identifier"};
 
+fun same_name (p,q) = #1(dest_atom p) = #1(dest_atom q);
 
 local fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s}
       fun single [_$_] = 
 	      mk_functional_err "recdef does not allow currying"
         | single [f] = f
-        | single fs  = mk_functional_err (Int.toString (length fs) ^ 
-                                          " distinct function names!")
+        | single fs  = 
+	      (*multiple function names?*)
+	      if length (gen_distinct same_name fs) < length fs
+              then mk_functional_err
+		   "the function being declared appears with multiple types"
+	      else mk_functional_err 
+		   (Int.toString (length fs) ^ 
+		    " distinct function names being declared")
 in
 fun mk_functional thy clauses =
  let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses)