eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;
--- 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;
-