# HG changeset patch
# User wenzelm
# Date 1159479769 -7200
# Node ID 468af396cf6f9254e57168dd87c4aae56fe44086
# Parent  7a51ed817ec79a108ff282e29a5c43326dcd049f
removed legacy code;
tuned;

diff -r 7a51ed817ec7 -r 468af396cf6f src/HOL/Tools/res_atpset.ML
--- a/src/HOL/Tools/res_atpset.ML	Thu Sep 28 23:42:47 2006 +0200
+++ b/src/HOL/Tools/res_atpset.ML	Thu Sep 28 23:42:49 2006 +0200
@@ -1,141 +1,41 @@
 (*  ID:         $Id$
-    Author:     Jia Meng, NICTA 
+    Author:     Jia Meng, NICTA
 
-Set of rules used for ATPs
+ATP rules.
 *)
 
 signature RES_ATPSET =
 sig
-    type atpset
-    val local_AtpSet_of: Proof.context -> atpset
-    val add_atp_rules: atpset * Thm.thm list -> atpset
-    val del_atp_rules: atpset * Thm.thm list -> atpset
-    val get_AtpSet: theory -> atpset
-    val print_local_AtpSet: Proof.context -> unit
-    val AtpSet_of: theory -> atpset
-    val add_atp_rule: Thm.thm * atpset -> atpset
-    val del_atp_rule: Thm.thm * atpset -> atpset
-    val print_atpset: atpset -> unit
-    val setup: theory -> theory
-    val get_local_AtpSet: Proof.context -> atpset
-    val rep_as: atpset -> Thm.thm list
-    val merge_atpset: atpset * atpset -> atpset
-    val add_atp_rule': Thm.thm -> atpset -> atpset
-    val del_atp_rule': Thm.thm -> atpset -> atpset
-    val Add_AtpRs: Thm.thm list -> unit
-    val Del_AtpRs: Thm.thm list -> unit
-    val empty_atpset: atpset
-    val put_local_AtpSet: atpset -> Proof.context -> Proof.context
-    val print_AtpSet: theory -> unit
-    val atp_rules_of_thy: theory -> Thm.thm list
-    val atp_rules_of_ctxt: Proof.context -> Thm.thm list
+  val print_atpset: Context.generic -> unit
+  val get_atpset: Context.generic -> thm list
+  val atp_add: attribute
+  val atp_del: attribute
+  val setup: theory -> theory
 end;
 
-
-
-structure ResAtpSet : RES_ATPSET =
-
+structure ResAtpset: RES_ATPSET =
 struct
 
-datatype atpset = AtpSet of thm list
-
-
-val mem_thm = member Drule.eq_thm_prop;
-val rem_thm = remove Drule.eq_thm_prop;
-
-val empty_atpset = AtpSet [];
-
-fun add_atp_rule (thm,AtpSet thms) = 
-    if mem_thm thms thm then (warning ("Ignoring duplicate ATP rules\n" ^ string_of_thm thm); AtpSet thms)
-    else
-	AtpSet (thm::thms);
-
-fun add_atp_rule' thm ars = add_atp_rule (thm,ars);
-fun add_atp_rules (ars,thms) =  foldl add_atp_rule ars thms;
-
-fun del_atp_rule (thm,AtpSet thms) = 
-    if mem_thm thms thm then AtpSet (rem_thm thm thms)
-    else
-	(warning "Undeclared rule for ATPs"; AtpSet thms);
-
-fun del_atp_rule' thm ars = del_atp_rule (thm,ars);
-
-fun del_atp_rules (ars,thms) = foldl del_atp_rule ars thms;
-
-fun merge_atpset (ars1, AtpSet thms2) = add_atp_rules (ars1,thms2);
-
-fun print_atpset (AtpSet thms) =
-    let val pretty_thms = map Display.pretty_thm in
-	[Pretty.big_list "Rules for ATPs:" (pretty_thms thms)]
-	    |> Pretty.chunks |> Pretty.writeln
-    end;
-
-fun rep_as (AtpSet thms) = thms;
-
-(* global AtpSet *)
-
-structure GlobalAtpSet = TheoryDataFun
-(struct
-  val name = "AtpSet";
-  type T = atpset ref;
-  
-  val empty = ref empty_atpset;
-  fun copy (ref atpst) = ref atpst : T;
-  val extend = copy;
-  fun merge _ (ref atpst1, ref atpst2) =
-      ref (merge_atpset (atpst1, atpst2));
-  fun print _ (ref atpst) = print_atpset atpst;
-end);
+structure Data = GenericDataFun
+(
+  val name = "HOL/atpset";
+  type T = thm list;
+  val empty = [];
+  val extend = I;
+  fun merge _ = Drule.merge_rules;
+  fun print context rules =
+    Pretty.writeln (Pretty.big_list "ATP rules:"
+      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
+);
 
-val print_AtpSet = GlobalAtpSet.print; 
-val get_AtpSet = ! o GlobalAtpSet.get;
-
-val change_AtpSet_of = change o GlobalAtpSet.get;
-fun change_AtpSet f = change_AtpSet_of (Context.the_context ()) f;
-
-
-fun AtpSet_of thy = get_AtpSet thy;
-
-fun Add_AtpRs args = change_AtpSet (fn ars => add_atp_rules (ars,args));
-
-fun Del_AtpRs args = change_AtpSet (fn ars => del_atp_rules (ars,args));
-
-fun atp_rules_of_thy thy = rep_as (AtpSet_of thy);
-
-(* local AtpSet *)
-
-structure LocalAtpSet = ProofDataFun
-(struct
-  val name = "AtpSet";
-  type T = atpset;
-  val init = get_AtpSet;
-  fun print _ atpst = print_atpset atpst;
-end);
+val print_atpset = Data.print;
+val get_atpset = Data.get;
 
-val print_local_AtpSet = LocalAtpSet.print;
-
-val get_local_AtpSet = LocalAtpSet.get;
-
-val put_local_AtpSet = LocalAtpSet.put;
-
-fun local_AtpSet_of ctxt = get_local_AtpSet ctxt;
-
-fun atp_rules_of_ctxt ctxt = rep_as (local_AtpSet_of ctxt);
+val atp_add = Thm.declaration_attribute (Data.map o Drule.add_rule);
+val atp_del = Thm.declaration_attribute (Data.map o Drule.del_rule);
 
-(* attributes *)
-fun attrib f = Thm.declaration_attribute (fn th =>
-   fn Context.Theory thy => (change_AtpSet_of thy (f th); Context.Theory thy)
-    | Context.Proof ctxt => Context.Proof (LocalAtpSet.map (f th) ctxt));
-
-
-val add_rule = attrib add_atp_rule';
-val del_rule = attrib del_atp_rule';
-
-val atpN = "atp";
-
-val setup_attrs = Attrib.add_attributes
-[(atpN, Attrib.add_del_args add_rule del_rule, "declaration of ATP rules")];
-
-val setup = GlobalAtpSet.init #> LocalAtpSet.init #> setup_attrs;
+val setup =
+  Data.init #>
+  Attrib.add_attributes [("atp", Attrib.add_del_args atp_add atp_del, "declaration of ATP rules")];
 
 end;