--- a/src/HOL/Tools/Function/decompose.ML Fri Oct 23 15:33:19 2009 +0200
+++ b/src/HOL/Tools/Function/decompose.ML Fri Oct 23 16:22:10 2009 +0200
@@ -33,8 +33,8 @@
Const (@{const_name Set.empty}, fastype_of c1))
|> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
- val chain = case FundefLib.try_proof (cterm_of thy goal) chain_tac of
- FundefLib.Solved thm => SOME thm
+ val chain = case Function_Lib.try_proof (cterm_of thy goal) chain_tac of
+ Function_Lib.Solved thm => SOME thm
| _ => NONE
in
Termination.note_chain c1 c2 chain D
@@ -62,7 +62,7 @@
let
val is = map (fn c => find_index (curry op aconv c) cs') cs
in
- CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv is))) i
+ CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv is))) i
end)