standard congs;
authorwenzelm
Wed Jul 23 12:54:49 1997 +0200 (1997-07-23 ago)
changeset 3566c9c351374651
parent 3565 c64410e701fb
child 3567 e2539e1980b4
standard congs;
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Wed Jul 23 11:54:32 1997 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Wed Jul 23 12:54:49 1997 +0200
     1.3 @@ -190,9 +190,9 @@
     1.4  (*Add congruence rules for = or <-> (instead of ==) *)
     1.5  infix 4 addcongs delcongs;
     1.6  fun ss addcongs congs =
     1.7 -        ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
     1.8 +        ss addeqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
     1.9  fun ss delcongs congs =
    1.10 -        ss deleqcongs (congs RL [eq_reflection,iff_reflection]);
    1.11 +        ss deleqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
    1.12  
    1.13  fun Addcongs congs = (simpset := !simpset addcongs congs);
    1.14  fun Delcongs congs = (simpset := !simpset delcongs congs);