--- a/src/HOL/Tools/function_package/fundef_package.ML Thu Jun 12 22:41:03 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Jun 12 23:12:54 2008 +0200
@@ -138,7 +138,7 @@
val data = the (case term_opt of
SOME t => import_fundef_data (Syntax.read_term lthy t) (Context.Proof lthy)
| NONE => import_last_fundef (Context.Proof lthy))
- handle Option.Option => raise ERROR ("Not a function: " ^ quote (the_default "" term_opt))
+ handle Option.Option => error ("Not a function: " ^ quote (the_default "" term_opt))
val FundefCtxData {termination, R, ...} = data
val domT = domain_type (fastype_of R)