# HG changeset patch
# User blanchet
# Date 1449004897 -3600
# Node ID 99f1eaf70c3dc640699a5d1d441195a8c7d1c685
# Parent  f58d75535f666a8e474fdc61468c3b9c994df4c7
reverted inadvertently qfinished/pushed change r164eeb2ab675

diff -r f58d75535f66 -r 99f1eaf70c3d src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Dec 01 17:18:34 2015 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Dec 01 22:21:37 2015 +0100
@@ -66,6 +66,11 @@
 
 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 =
@@ -405,7 +410,7 @@
 
 fun transfer_fp_sugars_interpretation fp_sugar lthy =
   let
-    val lthy = lthy |> (is_Type o T_of_bnf o bnf_of_fp_sugar) fp_sugar ? pred_injects fp_sugar
+    val lthy = pred_injects fp_sugar lthy
     val transfer_rules_notes = fp_sugar_transfer_rules fp_sugar
   in
     lthy
@@ -414,6 +419,7 @@
   end
 
 val _ =
-  Theory.setup (fp_sugars_interpretation transfer_plugin (fold transfer_fp_sugars_interpretation))
+  Theory.setup (fp_sugars_interpretation transfer_plugin
+    (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
 
 end