# 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)