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