# 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; -