# HG changeset patch
# User nipkow
# Date 1528376898 -7200
# Node ID 6a0852b8e5a8cff58a00a9e6e24724051c7d051b
# Parent  05605481935d99e06d7cd7ccf498a9e4e71352c5
comments

diff -r 05605481935d -r 6a0852b8e5a8 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Wed Jun 06 18:20:03 2018 +0200
+++ b/src/Pure/raw_simplifier.ML	Thu Jun 07 15:08:18 2018 +0200
@@ -591,6 +591,27 @@
   let val rews = extract_rews ctxt sym (map (Thm.transfer' ctxt) thms);
   in fold (fold comb o mk_rrule) rews ctxt end;
 
+(*
+This code checks if the symetric version of a rule is already in the simpset.
+However, the variable names in the two versions of the rule may differ.
+Thus the current test modulo eq_rrule is too weak to be useful
+and needs to be refined.
+
+fun present ctxt rules (rrule as {thm, elhs, ...}) =
+  (Net.insert_term eq_rrule (Thm.term_of elhs, trim_context_rrule rrule) rules;
+   false)
+  handle Net.INSERT =>
+    (cond_warning ctxt
+       (fn () => print_thm ctxt "Symmetric rewrite rule already in simpset:" ("", thm));
+     true);
+
+fun sym_present ctxt thms =
+  let
+    val rews = extract_rews ctxt true (map (Thm.transfer' ctxt) thms);
+    val rrules = map mk_rrule2 (flat(map (mk_rrule ctxt) rews))
+    val Simpset({rules, ...},_) = simpset_of ctxt
+  in exists (present ctxt rules) rrules end
+*)
 in
 
 fun ctxt addsimps thms =
@@ -606,6 +627,12 @@
   comb_simps ctxt (del_rrule false) (map mk_rrule2 o mk_rrule ctxt) false thms;
 
 fun add_simp thm ctxt = ctxt addsimps [thm];
+(*
+with check for presence of symmetric version:
+  if sym_present ctxt [thm]
+  then (cond_warning ctxt (fn () => print_thm ctxt "Ignoring rewrite rule:" ("", thm)); ctxt)
+  else ctxt addsimps [thm];
+*)
 fun del_simp thm ctxt = ctxt delsimps [thm];
 fun flip_simp thm ctxt = addsymsimps (delsimps_quiet ctxt [thm]) [thm];