--- a/src/HOL/Tools/Lifting/lifting_info.ML Sat Aug 16 20:14:45 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Sat Aug 16 20:27:51 2014 +0200
@@ -277,13 +277,8 @@
(* theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate *)
-structure Relator_Eq_Onp = Named_Thms
-(
- val name = @{binding relator_eq_onp}
- val description = "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate"
-)
-
-fun get_relator_eq_onp_rules ctxt = map safe_mk_meta_eq (Relator_Eq_Onp.get ctxt)
+fun get_relator_eq_onp_rules ctxt =
+ map safe_mk_meta_eq (rev (Named_Theorems.get ctxt @{named_theorems relator_eq_onp}))
(* info about reflexivity rules *)
@@ -525,12 +520,13 @@
val setup =
quot_map_attribute_setup
#> quot_del_attribute_setup
- #> Relator_Eq_Onp.setup
#> relator_distr_attribute_setup
(* setup fixed eq_onp rules *)
-val _ = Context.>> (fold (Relator_Eq_Onp.add_thm o Transfer.prep_transfer_domain_thm @{context})
+val _ = Context.>>
+ (fold (Named_Theorems.add_thm @{named_theorems relator_eq_onp} o
+ Transfer.prep_transfer_domain_thm @{context})
@{thms composed_equiv_rel_eq_onp composed_equiv_rel_eq_eq_onp})
(* setup fixed reflexivity rules *)