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