diff -r 67afe7e6a516 -r 77cd4992edcd src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Fri Dec 19 11:20:07 2014 +0100
+++ b/src/HOL/Transfer.thy	Fri Dec 19 14:06:13 2014 +0100
@@ -6,7 +6,7 @@
 section {* Generic theorem transfer using relations *}
 
 theory Transfer
-imports Hilbert_Choice Metis Basic_BNF_LFPs
+imports Basic_BNF_LFPs Hilbert_Choice Metis
 begin
 
 subsection {* Relator for function space *}
@@ -361,7 +361,21 @@
 
 end
 
+lemma if_conn:
+  "(if P \<and> Q then t else e) = (if P then if Q then t else e else e)"
+  "(if P \<or> Q then t else e) = (if P then t else if Q then t else e)"
+  "(if P \<longrightarrow> Q then t else e) = (if P then if Q then t else e else t)"
+  "(if \<not> P then t else e) = (if P then e else t)"
+by auto
+
 ML_file "Tools/Transfer/transfer_bnf.ML"
+ML_file "Tools/BNF/bnf_fp_rec_sugar_transfer.ML"
+
+ML {*
+val _ = Theory.setup (BNF_LFP_Rec_Sugar.primrec_interpretation
+  BNF_FP_Rec_Sugar_Transfer.primrec_transfer_pluginN
+  BNF_FP_Rec_Sugar_Transfer.primrec_transfer_interpretation)
+*}
 
 declare pred_fun_def [simp]
 declare rel_fun_eq [relator_eq]