Removed (term_of o cterm_of)-Hack, Added error message for unknown definition at "termination"-command
authorkrauss
Wed Jun 21 11:44:50 2006 +0200 (2006-06-21)
changeset 19938241a7777a3ff
parent 19937 d1b8374d8df7
child 19939 242b7312374d
Removed (term_of o cterm_of)-Hack, Added error message for unknown definition at "termination"-command
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Jun 21 11:24:19 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Jun 21 11:44:50 2006 +0200
     1.3 @@ -90,7 +90,6 @@
     1.4  	val congs = get_fundef_congs (Context.Theory thy)
     1.5  
     1.6  	val t_eqns = map (map (Sign.read_prop thy)) eqns
     1.7 -			 |> map (map (term_of o cterm_of thy)) (* HACK to prevent strange things from happening with abbreviations *)
     1.8  
     1.9  	val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy
    1.10  	val Prep {goal, goalI, ...} = data
    1.11 @@ -160,6 +159,7 @@
    1.12      let
    1.13  	val name = if name = "" then get_last_fundef thy else name
    1.14  	val data = the (get_fundef_data name thy)
    1.15 +                   handle Option.Option => raise ERROR ("No such function definition: " ^ name)
    1.16  
    1.17  	val (res as FundefMResult {termination, ...}, mutual, _, _) = data
    1.18  	val goal = FundefTermination.mk_total_termination_goal data