# HG changeset patch
# User wenzelm
# Date 909052540 -7200
# Node ID 1d1175ef2d560efb2a865b3344bd59f400bc6089
# Parent  1b708bfb0c1e50320a8f2fb343b514da04d3b42e
eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;

diff -r 1b708bfb0c1e -r 1d1175ef2d56 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Thu Oct 22 12:32:42 1998 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Thu Oct 22 12:35:40 1998 +0200
@@ -43,9 +43,10 @@
 
 
 functor Abel_Cancel (Data: ABEL_CANCEL) =
-let open Data in
 struct
 
+open Data;
+
  val prepare_ss = Data.ss addsimps [add_assoc, diff_def, 
 				    minus_add_distrib, minus_minus,
 				    minus_0, add_0, add_0_right];
@@ -189,6 +190,4 @@
        (map (Thm.cterm_of (sign_of Data.thy) o Data.dest_eqI) eqI_rules)
        rel_proc;
 
- end
 end;
-