--- 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;