Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors
authorpaulson
Wed Mar 05 10:07:04 1997 +0100 (1997-03-05 ago)
changeset 2727230f2643107e
parent 2726 e050f8bb1177
child 2728 df3a269b6f34
Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Wed Mar 05 10:05:32 1997 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Wed Mar 05 10:07:04 1997 +0100
     1.3 @@ -306,16 +306,16 @@
     1.4  
     1.5  infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
     1.6  	addsimps2 delsimps2 addcongs2 delcongs2;
     1.7 -val op addSIs2   = pair_upd1 (op addSIs);
     1.8 -val op addSEs2   = pair_upd1 (op addSEs);
     1.9 -val op addSDs2   = pair_upd1 (op addSDs);
    1.10 -val op addIs2    = pair_upd1 (op addIs );
    1.11 -val op addEs2    = pair_upd1 (op addEs );
    1.12 -val op addDs2    = pair_upd1 (op addDs );
    1.13 -val op addsimps2 = pair_upd2 (op addsimps);
    1.14 -val op delsimps2 = pair_upd2 (op delsimps);
    1.15 -val op addcongs2 = pair_upd2 (op addcongs);
    1.16 -val op delcongs2 = pair_upd2 (op delcongs);
    1.17 +fun op addSIs2   arg = pair_upd1 (op addSIs) arg;
    1.18 +fun op addSEs2   arg = pair_upd1 (op addSEs) arg;
    1.19 +fun op addSDs2   arg = pair_upd1 (op addSDs) arg;
    1.20 +fun op addIs2    arg = pair_upd1 (op addIs ) arg;
    1.21 +fun op addEs2    arg = pair_upd1 (op addEs ) arg;
    1.22 +fun op addDs2    arg = pair_upd1 (op addDs ) arg;
    1.23 +fun op addsimps2 arg = pair_upd2 (op addsimps) arg;
    1.24 +fun op delsimps2 arg = pair_upd2 (op delsimps) arg;
    1.25 +fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
    1.26 +fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
    1.27  
    1.28  fun auto_tac (cs,ss) = let val cs' = cs addss ss in
    1.29  EVERY [	TRY (safe_tac cs'),