--- a/src/Provers/Arith/fast_lin_arith.ML Mon Oct 17 23:10:13 2005 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Mon Oct 17 23:10:15 2005 +0200
@@ -417,7 +417,7 @@
fun mkthm (sg, ss) asms just =
let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
Data.get sg;
- val simpset' = Simplifier.inherit_bounds ss simpset;
+ val simpset' = Simplifier.inherit_context ss simpset;
val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) =>
map fst lhs union (map fst rhs union ats))
([], List.mapPartial (fn thm => if Thm.no_prems thm