--- a/src/HOL/Tools/function_package/fundef_prep.ML Thu Nov 30 14:17:22 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML Thu Nov 30 14:17:25 2006 +0100
@@ -237,7 +237,7 @@
|> fold_rev (implies_intr o cprop_of) h_assums
|> fold_rev (implies_intr o cprop_of) ags
|> fold_rev forall_intr cqs
- |> Drule.close_derivation
+ |> Goal.close_result
in
replace_lemma
end
@@ -367,7 +367,7 @@
|> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
val goal = complete COMP (graph_is_function COMP conjunctionI)
- |> Drule.close_derivation
+ |> Goal.close_result
val goalI = Goal.protect goal
|> fold_rev (implies_intr o cprop_of) compat