src/Pure/Isar/calculation.ML
changeset 12402 cef751fff6b0
parent 12379 c74d160ff0c5
child 12805 3be853cf19cf
     1.1 --- a/src/Pure/Isar/calculation.ML	Thu Dec 06 00:41:37 2001 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Thu Dec 06 00:42:00 2001 +0100
     1.3 @@ -102,9 +102,9 @@
     1.4  val trans_del_local = local_att (apfst o NetRules.delete);
     1.5  
     1.6  val sym_add_global = global_att (apsnd o Drule.add_rule) o ContextRules.elim_query_global None;
     1.7 -val sym_del_global = global_att (apsnd o Drule.del_rule);
     1.8 +val sym_del_global = global_att (apsnd o Drule.del_rule) o ContextRules.rule_del_global;
     1.9  val sym_add_local = local_att (apsnd o Drule.add_rule) o ContextRules.elim_query_local None;
    1.10 -val sym_del_local = local_att (apsnd o Drule.del_rule);
    1.11 +val sym_del_local = local_att (apsnd o Drule.del_rule) o ContextRules.rule_del_local;
    1.12  
    1.13  
    1.14  (* symmetry *)