src/HOL/Tools/Transfer/transfer.ML

 *)
 
 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
   val top_sweep_rewr_conv: thm list -> conv
 

 
 val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o apply2 snd) (single o fst);
 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}
-
-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
+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}
+
+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
 (
   type T =
     { transfer_raw : thm Item_Net.T,

   Attrib.thms >> transferred_attribute
 
 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)))
 
 fun update_pred_data type_name qinfo ctxt =