# HG changeset patch
# User paulson
# Date 925723148 -7200
# Node ID 7ed743d18af702da656d648cbb0d205942eeaa9b
# Parent  de4acf4449fa6d23e9be9fca256767cd1c4c0855
improved error handling

diff -r de4acf4449fa -r 7ed743d18af7 TFL/tfl.sml
--- a/TFL/tfl.sml	Mon May 03 11:18:44 1999 +0200
+++ b/TFL/tfl.sml	Mon May 03 11:19:08 1999 +0200
@@ -289,13 +289,17 @@
  end;
 
 local fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s}
-      fun single [f] = f
+      fun single [Free(a,_)] = 
+	      mk_functional_err (a ^ " has not been declared as a constant")
+        | single [f] = f
         | single fs  = mk_functional_err (Int.toString (length fs) ^ 
                                           " distinct function names!")
 in
 fun mk_functional thy clauses =
- let val (L,R) = ListPair.unzip 
-                    (map (fn (Const("op =",_) $ t $ u) => (t,u)) clauses)
+ let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses)
+                   handle _ => raise TFL_ERR
+		       {func = "mk_functional", 
+			mesg = "recursion equations must use the = relation"}
      val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
      val fcon as Const (fname, ftype) = single (gen_distinct (op aconv) funcs)
      val dummy = map (no_repeat_vars thy) pats