# HG changeset patch
# User wenzelm
# Date 1350851542 -7200
# Node ID 69774b4f5b8af9082f487d992bb6ef6d507c5709
# Parent  cf4c03c019e59ace7009f2f6b9814a4ab75ba8a2
recovered explicit error message, which was lost in b8570ea1ce25;

diff -r cf4c03c019e5 -r 69774b4f5b8a src/HOL/Tools/Function/function.ML
--- 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