# HG changeset patch
# User wenzelm
# Date 1007595720 -3600
# Node ID cef751fff6b096f229b6e18f2948de3acad87a15
# Parent  4363432ef0cddf251b2e7d40595dc0574c961d83
clarified sym_del;

diff -r 4363432ef0cd -r cef751fff6b0 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Thu Dec 06 00:41:37 2001 +0100
+++ b/src/Pure/Isar/calculation.ML	Thu Dec 06 00:42:00 2001 +0100
@@ -102,9 +102,9 @@
 val trans_del_local = local_att (apfst o NetRules.delete);
 
 val sym_add_global = global_att (apsnd o Drule.add_rule) o ContextRules.elim_query_global None;
-val sym_del_global = global_att (apsnd o Drule.del_rule);
+val sym_del_global = global_att (apsnd o Drule.del_rule) o ContextRules.rule_del_global;
 val sym_add_local = local_att (apsnd o Drule.add_rule) o ContextRules.elim_query_local None;
-val sym_del_local = local_att (apsnd o Drule.del_rule);
+val sym_del_local = local_att (apsnd o Drule.del_rule) o ContextRules.rule_del_local;
 
 
 (* symmetry *)