src/HOL/MiniML/W.ML

--- a/src/HOL/MiniML/W.ML	Thu Aug 20 10:17:18 1998 +0200
+++ b/src/HOL/MiniML/W.ML	Thu Aug 20 16:18:39 1998 +0200
@@ -8,7 +8,7 @@
 
 open W;
 
-Addsimps [diff_add_inverse,diff_add_inverse2,Suc_le_lessD];
+Addsimps [Suc_le_lessD];  Delsimps [less_imp_le];  (*the combination loops*)
 
 val has_type_casesE = map(has_type.mk_cases expr.simps)
         [" A |- Var n :: t"," A |- Abs e :: t","A |- App e1 e2 ::t","A |- LET e1 e2 ::t" ];