# HG changeset patch
# User krauss
# Date 1150883090 -7200
# Node ID 241a7777a3ffe6c400fd2ba662e0dc771f9c8217
# Parent  d1b8374d8df705022dbf1ef937e425dbd500951d
Removed (term_of o cterm_of)-Hack, Added error message for unknown definition at "termination"-command

diff -r d1b8374d8df7 -r 241a7777a3ff src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Jun 21 11:24:19 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Jun 21 11:44:50 2006 +0200
@@ -90,7 +90,6 @@
 	val congs = get_fundef_congs (Context.Theory thy)
 
 	val t_eqns = map (map (Sign.read_prop thy)) eqns
-			 |> map (map (term_of o cterm_of thy)) (* HACK to prevent strange things from happening with abbreviations *)
 
 	val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy
 	val Prep {goal, goalI, ...} = data
@@ -160,6 +159,7 @@
     let
 	val name = if name = "" then get_last_fundef thy else name
 	val data = the (get_fundef_data name thy)
+                   handle Option.Option => raise ERROR ("No such function definition: " ^ name)
 
 	val (res as FundefMResult {termination, ...}, mutual, _, _) = data
 	val goal = FundefTermination.mk_total_termination_goal data