recovered explicit error message, which was lost in b8570ea1ce25;

--- a/src/HOL/Tools/Function/function.ML	Sun Oct 21 22:31:39 2012 +0200
+++ b/src/HOL/Tools/Function/function.ML	Sun Oct 21 22:32:22 2012 +0200
@@ -168,11 +168,15 @@
   let
     val term_opt = Option.map (prep_term lthy) raw_term_opt
     val info =
-      the (case term_opt of
-             SOME t => (import_function_data t lthy
-               handle Option.Option =>
-                 error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
-           | NONE => (import_last_function lthy handle Option.Option => error "Not a function"))
+      (case term_opt of
+        SOME t =>
+          (case import_function_data t lthy of
+            SOME info => info
+          | NONE => error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
+      | NONE =>
+          (case import_last_function lthy of
+            SOME info => info
+          | NONE => error "Not a function"))
 
     val { termination, fs, R, add_simps, case_names, psimps,
       pinducts, defname, ...} = info