diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -1368,7 +1368,7 @@
           let
             val rel_conversep_thm = Lazy.force rel_conversep;
             val cts = map (SOME o Thm.cterm_of lthy) Rs;
-            val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm;
+            val rel_conversep_thm' = infer_instantiate' lthy cts rel_conversep_thm;
           in
             unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_eqD})
             |> singleton (Proof_Context.export names_lthy pre_names_lthy)