# HG changeset patch
# User blanchet
# Date 1448971661 -3600
# Node ID 164eeb2ab675bdbf03f3be1b226ce1e01a3612c6
# Parent  1647bb48952239c72fe5e493f7452242caf64562
set "transfer_rule" attribute more generously

diff -r 1647bb489522 -r 164eeb2ab675 src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Dec 01 13:07:40 2015 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Dec 01 13:07:41 2015 +0100
@@ -66,11 +66,6 @@
 
 fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
 
-fun fp_sugar_only_type_ctr f fp_sugars =
-  (case filter (is_Type o T_of_bnf o bnf_of_fp_sugar) fp_sugars of
-    [] => I
-  | fp_sugars' => f fp_sugars')
-
 (* relation constraints - bi_total & co. *)
 
 fun mk_relation_constraint name arg =
@@ -410,7 +405,7 @@
 
 fun transfer_fp_sugars_interpretation fp_sugar lthy =
   let
-    val lthy = pred_injects fp_sugar lthy
+    val lthy = lthy |> (is_Type o T_of_bnf o bnf_of_fp_sugar) fp_sugar ? pred_injects fp_sugar
     val transfer_rules_notes = fp_sugar_transfer_rules fp_sugar
   in
     lthy
@@ -419,7 +414,6 @@
   end
 
 val _ =
-  Theory.setup (fp_sugars_interpretation transfer_plugin
-    (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
+  Theory.setup (fp_sugars_interpretation transfer_plugin (fold transfer_fp_sugars_interpretation))
 
 end