| changeset 9720 | 3b7b72db57f1 |
| parent 9715 | 5705a04d24ea |
| child 9861 | b2a6d854d6da |
--- a/src/Provers/simplifier.ML Tue Aug 29 12:08:20 2000 +0200 +++ b/src/Provers/simplifier.ML Tue Aug 29 12:28:48 2000 +0200 @@ -504,7 +504,7 @@ Scan.succeed asm_full_simp_tac); val cong_modifiers = - [Args.$$$ congN -- Args.colon >> K (I, cong_add_local), + [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier), Args.$$$ congN -- Args.$$$ addN -- Args.colon >> K (I, cong_add_local), Args.$$$ congN -- Args.$$$ delN -- Args.colon >> K (I, cong_del_local)];