updated to named_theorems;
authorwenzelm
Sat Aug 16 13:54:19 2014 +0200 (2014-08-16)
changeset 57949b203a7644bf1
parent 57948 75724d71013c
child 57950 59c17b0b870d
updated to named_theorems;
src/Tools/atomize_elim.ML
     1.1 --- a/src/Tools/atomize_elim.ML	Sat Aug 16 13:23:50 2014 +0200
     1.2 +++ b/src/Tools/atomize_elim.ML	Sat Aug 16 13:54:19 2014 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  signature ATOMIZE_ELIM =
     1.6  sig
     1.7 -  val declare_atomize_elim : attribute
     1.8    val atomize_elim_conv : Proof.context -> conv
     1.9    val full_atomize_elim_conv : Proof.context -> conv
    1.10    val atomize_elim_tac : Proof.context -> int -> tactic
    1.11 @@ -15,17 +14,14 @@
    1.12  structure Atomize_Elim : ATOMIZE_ELIM =
    1.13  struct
    1.14  
    1.15 -(* theory data *)
    1.16 +(* atomize_elim rules *)
    1.17  
    1.18 -structure AtomizeElimData = Named_Thms
    1.19 -(
    1.20 -  val name = @{binding atomize_elim};
    1.21 -  val description = "atomize_elim rewrite rule";
    1.22 -);
    1.23 +val named_theorems =
    1.24 +  Context.>>> (Context.map_theory_result
    1.25 +   (Named_Target.theory_init #>
    1.26 +    Named_Theorems.declare @{binding atomize_elim} "atomize_elim rewrite rule" ##>
    1.27 +    Local_Theory.exit_global));
    1.28  
    1.29 -val _ = Theory.setup AtomizeElimData.setup;
    1.30 -
    1.31 -val declare_atomize_elim = AtomizeElimData.add
    1.32  
    1.33  (* More conversions: *)
    1.34  local open Conv in
    1.35 @@ -58,7 +54,7 @@
    1.36  *)
    1.37  fun atomize_elim_conv ctxt ct =
    1.38      (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
    1.39 -    then_conv Raw_Simplifier.rewrite ctxt true (AtomizeElimData.get ctxt)
    1.40 +    then_conv Raw_Simplifier.rewrite ctxt true (Named_Theorems.get ctxt named_theorems)
    1.41      then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
    1.42                           then all_conv ct'
    1.43                           else raise CTERM ("atomize_elim", [ct', ct])))