src/Provers/classical.ML
changeset 18643 89a7978f90e1
parent 18586 588e80289658
child 18688 abf0f018b5ec
     1.1 --- a/src/Provers/classical.ML	Tue Jan 10 19:33:42 2006 +0100
     1.2 +++ b/src/Provers/classical.ML	Tue Jan 10 19:34:04 2006 +0100
     1.3 @@ -968,7 +968,7 @@
     1.4  val haz_dest_global = change_global_cs (op addDs);
     1.5  val haz_elim_global = change_global_cs (op addEs);
     1.6  val haz_intro_global = change_global_cs (op addIs);
     1.7 -val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global;
     1.8 +val rule_del_global = change_global_cs (op delrules) o Attrib.theory ContextRules.rule_del;
     1.9  
    1.10  val safe_dest_local = change_local_cs (op addSDs);
    1.11  val safe_elim_local = change_local_cs (op addSEs);
    1.12 @@ -976,7 +976,7 @@
    1.13  val haz_dest_local = change_local_cs (op addDs);
    1.14  val haz_elim_local = change_local_cs (op addEs);
    1.15  val haz_intro_local = change_local_cs (op addIs);
    1.16 -val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local;
    1.17 +val rule_del_local = change_local_cs (op delrules) o Attrib.context ContextRules.rule_del;
    1.18  
    1.19  
    1.20  (* tactics referring to the implicit claset *)
    1.21 @@ -1019,16 +1019,16 @@
    1.22  val setup_attrs = Attrib.add_attributes
    1.23   [("swapped", (swapped, swapped), "classical swap of introduction rule"),
    1.24    (destN,
    1.25 -   (add_rule ContextRules.dest_query_global haz_dest_global safe_dest_global,
    1.26 -    add_rule ContextRules.dest_query_local haz_dest_local safe_dest_local),
    1.27 +   (add_rule (Attrib.theory o ContextRules.dest_query) haz_dest_global safe_dest_global,
    1.28 +    add_rule (Attrib.context o ContextRules.dest_query) haz_dest_local safe_dest_local),
    1.29      "declaration of destruction rule"),
    1.30    (elimN,
    1.31 -   (add_rule ContextRules.elim_query_global haz_elim_global safe_elim_global,
    1.32 -    add_rule ContextRules.elim_query_local haz_elim_local safe_elim_local),
    1.33 +   (add_rule (Attrib.theory o ContextRules.elim_query) haz_elim_global safe_elim_global,
    1.34 +    add_rule (Attrib.context o ContextRules.elim_query) haz_elim_local safe_elim_local),
    1.35      "declaration of elimination rule"),
    1.36    (introN,
    1.37 -   (add_rule ContextRules.intro_query_global haz_intro_global safe_intro_global,
    1.38 -    add_rule ContextRules.intro_query_local haz_intro_local safe_intro_local),
    1.39 +   (add_rule (Attrib.theory o ContextRules.intro_query) haz_intro_global safe_intro_global,
    1.40 +    add_rule (Attrib.context o ContextRules.intro_query) haz_intro_local safe_intro_local),
    1.41      "declaration of introduction rule"),
    1.42    (ruleN, (del_rule rule_del_global, del_rule rule_del_local),
    1.43      "remove declaration of intro/elim/dest rule")];