--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri May 27 20:23:55 2016 +0200
@@ -152,7 +152,7 @@
val th'' =
Goal.prove ctxt (Term.add_free_names t' []) [] t'
(fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt))
- val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
+ val th''' = Local_Defs.unfold0 ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
in
th'''
end;