Eta-expanded some declarations for compatibility with value polymorphism
authorpaulson
Fri Mar 07 10:20:26 1997 +0100 (1997-03-07)
changeset 27483ae9ccdd701e
parent 2747 9fdc1461085f
child 2749 2f477a0e690d
Eta-expanded some declarations for compatibility with value polymorphism
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Fri Mar 07 10:19:24 1997 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Fri Mar 07 10:20:26 1997 +0100
     1.3 @@ -410,16 +410,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'),