tuned; store pred_simps

--- a/src/HOL/Tools/Transfer/transfer.ML	Tue Nov 18 16:19:57 2014 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Nov 18 16:19:57 2014 +0100
@@ -8,9 +8,12 @@
 signature TRANSFER =
 sig
   type pred_data
+  val mk_pred_data: thm -> thm -> thm list -> pred_data
   val rel_eq_onp: pred_data -> thm
   val rel_eq_onp_with_tops: pred_data -> thm
   val pred_def: pred_data -> thm
+  val pred_simps: pred_data -> thm list
+  val update_pred_simps: thm list -> pred_data -> pred_data
 
   val bottom_rewr_conv: thm list -> conv
   val top_rewr_conv: thm list -> conv
@@ -59,13 +62,23 @@
 val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq
   o HOLogic.dest_Trueprop o Thm.concl_of);
 
-type pred_data = {pred_def:thm, rel_eq_onp: thm}
+datatype pred_data = PRED_DATA of {pred_def:thm, rel_eq_onp: thm, pred_simps: thm list}
+
+fun mk_pred_data pred_def rel_eq_onp pred_simps = PRED_DATA {pred_def = pred_def, 
+  rel_eq_onp = rel_eq_onp, pred_simps = pred_simps}
+
+fun map_pred_data' f1 f2 f3 (PRED_DATA {pred_def, rel_eq_onp, pred_simps}) =
+  PRED_DATA {pred_def = f1 pred_def, rel_eq_onp = f2 rel_eq_onp, pred_simps = f3 pred_simps}
 
-val rel_eq_onp: pred_data -> thm = #rel_eq_onp
-val rel_eq_onp_with_tops: pred_data -> thm = (Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
+fun rep_pred_data (PRED_DATA p) = p
+val rel_eq_onp = #rel_eq_onp o rep_pred_data
+val rel_eq_onp_with_tops = (Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
   (top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))))
-  o #rel_eq_onp
-val pred_def: pred_data -> thm = #pred_def
+  o #rel_eq_onp o rep_pred_data
+val pred_def = #pred_def o rep_pred_data
+val pred_simps = #pred_simps o rep_pred_data
+fun update_pred_simps new_pred_data = map_pred_data' I I (K new_pred_data)
+
 
 structure Data = Generic_Data
 (
@@ -796,9 +809,12 @@
 val untransferred_attribute_parser =
   Attrib.thms >> untransferred_attribute
 
-fun morph_pred_data phi {pred_def, rel_eq_onp} = 
-  {pred_def =  Morphism.thm phi pred_def,
-  rel_eq_onp = Morphism.thm phi rel_eq_onp}
+fun morph_pred_data phi = 
+  let
+    val morph_thm = Morphism.thm phi
+  in
+    map_pred_data' morph_thm morph_thm (map morph_thm)
+  end
 
 fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name
   |> Option.map (morph_pred_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))

--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Nov 18 16:19:57 2014 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Nov 18 16:19:57 2014 +0100
@@ -283,7 +283,7 @@
     fun qualify defname suffix = Binding.qualified true suffix defname
     val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel"
     val rel_eq_onp_thm_name = qualify (base_name_of_bnf bnf) "rel_eq_onp"
-    val pred_data = {pred_def = pred_def, rel_eq_onp = rel_eq_onp}
+    val pred_data = Transfer.mk_pred_data pred_def rel_eq_onp []
     val type_name = type_name_of_bnf bnf
     val relator_domain_attr = @{attributes [relator_domain]}
     val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)]),
@@ -398,18 +398,26 @@
     fun qualify defname suffix = Binding.qualified true suffix defname
     val pred_inject_thm_name = qualify (base_name_of_bnf (bnf_of_fp_sugar fp_sugar)) "pred_inject"
     val simp_attrs = @{attributes [simp]}
+    val type_name = type_name_of_bnf (#fp_bnf fp_sugar)
+    val pred_data = lookup_defined_pred_data lthy type_name 
+      |> Transfer.update_pred_simps pred_injects
   in
-    [((pred_inject_thm_name, []), [(pred_injects, simp_attrs)])]
+    lthy 
+    |> Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) 
+    |> snd
+    |> Local_Theory.declaration {syntax = false, pervasive = true}
+      (fn phi => Transfer.update_pred_data type_name  (Transfer.morph_pred_data phi pred_data))
+    |> Local_Theory.restore
   end
 
 
 fun transfer_fp_sugars_interpretation fp_sugar lthy =
   let
-    val pred_injects_notes = pred_injects fp_sugar lthy
+    val lthy = pred_injects fp_sugar lthy
     val transfer_rules_notes = fp_sugar_transfer_rules fp_sugar
   in
     lthy
-    |> Local_Theory.notes (pred_injects_notes @ transfer_rules_notes)
+    |> Local_Theory.notes transfer_rules_notes
     |> snd
   end