# HG changeset patch
# User nipkow
# Date 748191317 -7200
# Node ID 5f77582e3a89e72ec99dac10fe70743c0ba1d58e
# Parent  c67f44be880f34586a23582dd084e662016c2db3
defined local addcongs

diff -r c67f44be880f -r 5f77582e3a89 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu Sep 16 16:25:32 1993 +0200
+++ b/src/FOL/simpdata.ML	Thu Sep 16 16:55:17 1993 +0200
@@ -84,13 +84,17 @@
 
 open Simplifier Induction;
 
+infix addcongs;
+fun ss addcongs congs =
+  ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
+
 val IFOL_ss = empty_ss
       setmksimps mk_rew_rules
       setsolver
         (fn prems => resolve_tac (TrueI::refl::iff_refl::notFalseI::prems))
       setsubgoaler asm_simp_tac
       addsimps IFOL_rews
-      addcongs [imp_cong RS iff_reflection];
+      addcongs [imp_cong];
 
 (*Classical version...*)
 fun prove_fun s =