--- a/src/HOL/NSA/transfer.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/NSA/transfer.ML Sun Mar 07 11:57:16 2010 +0100
@@ -56,7 +56,7 @@
let
val thy = ProofContext.theory_of ctxt;
val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt);
- val meta = LocalDefs.meta_rewrite_rule ctxt;
+ val meta = Local_Defs.meta_rewrite_rule ctxt;
val ths' = map meta ths;
val unfolds' = map meta unfolds and refolds' = map meta refolds;
val (_$_$t') = concl_of (MetaSimplifier.rewrite true unfolds' (cterm_of thy t))