# HG changeset patch
# User wenzelm
# Date 1408190059 -7200
# Node ID b203a7644bf1e82582c3c8bb40c46907e6e2c104
# Parent  75724d71013c77dc0787663000ea7f09cd98bbd1
updated to named_theorems;

diff -r 75724d71013c -r b203a7644bf1 src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Sat Aug 16 13:23:50 2014 +0200
+++ b/src/Tools/atomize_elim.ML	Sat Aug 16 13:54:19 2014 +0200
@@ -6,7 +6,6 @@
 
 signature ATOMIZE_ELIM =
 sig
-  val declare_atomize_elim : attribute
   val atomize_elim_conv : Proof.context -> conv
   val full_atomize_elim_conv : Proof.context -> conv
   val atomize_elim_tac : Proof.context -> int -> tactic
@@ -15,17 +14,14 @@
 structure Atomize_Elim : ATOMIZE_ELIM =
 struct
 
-(* theory data *)
+(* atomize_elim rules *)
 
-structure AtomizeElimData = Named_Thms
-(
-  val name = @{binding atomize_elim};
-  val description = "atomize_elim rewrite rule";
-);
+val named_theorems =
+  Context.>>> (Context.map_theory_result
+   (Named_Target.theory_init #>
+    Named_Theorems.declare @{binding atomize_elim} "atomize_elim rewrite rule" ##>
+    Local_Theory.exit_global));
 
-val _ = Theory.setup AtomizeElimData.setup;
-
-val declare_atomize_elim = AtomizeElimData.add
 
 (* More conversions: *)
 local open Conv in
@@ -58,7 +54,7 @@
 *)
 fun atomize_elim_conv ctxt ct =
     (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
-    then_conv Raw_Simplifier.rewrite ctxt true (AtomizeElimData.get ctxt)
+    then_conv Raw_Simplifier.rewrite ctxt true (Named_Theorems.get ctxt named_theorems)
     then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
                          then all_conv ct'
                          else raise CTERM ("atomize_elim", [ct', ct])))