diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sun Mar 07 11:57:16 2010 +0100
@@ -145,7 +145,7 @@
     val t' = Pattern.rewrite_term thy rewr [] t
     val tac = Skip_Proof.cheat_tac thy
     val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac)
-    val th''' = LocalDefs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
+    val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
   in
     th'''
   end;