# HG changeset patch
# User wenzelm
# Date 1408213671 -7200
# Node ID 10b2f60b70f0b65e9e12de500828813a2a2dd5d1
# Parent  ee1ba48488960bd7ee046df5effc6fa38000cc18
updated to named_theorems;

diff -r ee1ba4848896 -r 10b2f60b70f0 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Sat Aug 16 20:14:45 2014 +0200
+++ b/src/HOL/Lifting.thy	Sat Aug 16 20:27:51 2014 +0200
@@ -545,6 +545,8 @@
 
 ML_file "Tools/Lifting/lifting_util.ML"
 
+named_theorems relator_eq_onp
+  "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate"
 ML_file "Tools/Lifting/lifting_info.ML"
 setup Lifting_Info.setup
 
diff -r ee1ba4848896 -r 10b2f60b70f0 src/HOL/Tools/Lifting/lifting_info.ML
--- 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 *)