diff -r dd84daec5d3c -r 2ad95934521f src/HOL/Tools/Function/function_common.ML
--- 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:"