improved error message for common mistake (fun f where "g x = ...")

--- a/src/HOL/Tools/Function/fun.ML	Fri Sep 10 10:59:10 2010 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Fri Sep 10 14:37:57 2010 +0200
@@ -44,7 +44,7 @@
          ())
       end
 
-    val (_, qs, gs, args, _) = split_def ctxt geq
+    val (_, qs, gs, args, _) = split_def ctxt (K true) geq
 
     val _ = if not (null gs) then err "Conditional equations" else ()
     val _ = map check_constr_pattern args
@@ -76,7 +76,7 @@
   end
 
 fun add_catchall ctxt fixes spec =
-  let val fqgars = map (split_def ctxt) spec
+  let val fqgars = map (split_def ctxt (K true)) spec
       val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
                      |> AList.lookup (op =) #> the
   in

--- a/src/HOL/Tools/Function/function_common.ML	Fri Sep 10 10:59:10 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Fri Sep 10 14:37:57 2010 +0200
@@ -215,7 +215,7 @@
 
 (* Analyzing function equations *)
 
-fun split_def ctxt geq =
+fun split_def ctxt check_head geq =
   let
     fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
     val qs = Term.strip_qnt_vars "all" geq
@@ -227,8 +227,8 @@
 
     val (head, args) = strip_comb f_args
 
-    val fname = fst (dest_Free head)
-      handle TERM _ => error (input_error "Head symbol must not be a bound variable")
+    val fname = fst (dest_Free head) handle TERM _ => ""
+    val _ = check_head fname
   in
     (fname, qs, gs, args, rhs)
   end
@@ -242,11 +242,11 @@
       let
         fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
 
-        val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
+        fun check_head fname =
+          member (op =) fnames fname orelse
+          input_error ("Illegal equation head. Expected " ^ commas_quote fnames)
 
-        val _ = member (op =) fnames fname 
-          orelse input_error ("Head symbol of left hand side must be " ^
-            plural "" "one out of " fnames ^ commas_quote fnames)
+        val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq
 
         val _ = length args > 0 orelse input_error "Function has no arguments:"
 

--- a/src/HOL/Tools/Function/mutual.ML	Fri Sep 10 10:59:10 2010 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Fri Sep 10 14:37:57 2010 +0200
@@ -72,7 +72,7 @@
 fun analyze_eqs ctxt defname fs eqs =
   let
     val num = length fs
-    val fqgars = map (split_def ctxt) eqs
+    val fqgars = map (split_def ctxt (K true)) eqs
     val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
       |> AList.lookup (op =) #> the