diff -r f6e351043014 -r 1e1782c1aedf src/HOL/Library/conditional_parametricity.ML
--- a/src/HOL/Library/conditional_parametricity.ML	Sat Feb 17 20:03:37 2018 +0100
+++ b/src/HOL/Library/conditional_parametricity.ML	Sun Feb 18 15:05:21 2018 +0100
@@ -457,7 +457,7 @@
       Option.filter (is_parametricity_theorem andf (not o curry Term.could_unify
         (Thm.full_prop_of @{thm is_equality_Rel})) o Thm.full_prop_of) o preprocess_theorem ctxt;
   in
-    map_filter (parametricity_thm_map_filter o Thm.transfer (Proof_Context.theory_of ctxt))
+    map_filter (parametricity_thm_map_filter o Thm.transfer' ctxt)
       (Transfer.get_transfer_raw ctxt)
   end;