--- a/src/HOL/Tools/BNF/bnf_def.ML Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Apr 23 10:23:27 2014 +0200
@@ -941,8 +941,8 @@
||>> mk_Frees "R" transfer_domRTs
||>> mk_Frees "S" transfer_ranRTs;
- val fs_copy = map2 (retype_free o fastype_of) fs gs;
- val x_copy = retype_free CA' y;
+ val fs_copy = map2 (retype_const_or_free o fastype_of) fs gs;
+ val x_copy = retype_const_or_free CA' y;
val rel = mk_bnf_rel pred2RTs CA' CB';
val relAsAs = mk_bnf_rel self_pred2RTs CA' CA';