# HG changeset patch
# User wenzelm
# Date 967544928 -7200
# Node ID 3b7b72db57f11234a7f77b5af9e590346540c4ee
# Parent  c753196599f90838a2c4d0b813f42e139dec1b69
made SML/XL happy;

diff -r c753196599f9 -r 3b7b72db57f1 src/Provers/simplifier.ML
--- 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)];