# HG changeset patch # User wenzelm # Date 1385222831 -3600 # Node ID 63e4474fd0ed882cdc1b46b290488b439fc373d2 # Parent 5df6e746ad0374e3dda33a2a3cb85fdec9919dda tuned; diff -r 5df6e746ad03 -r 63e4474fd0ed src/Provers/Arith/cancel_numerals.ML --- a/src/Provers/Arith/cancel_numerals.ML Sat Nov 23 16:39:08 2013 +0100 +++ b/src/Provers/Arith/cancel_numerals.ML Sat Nov 23 17:07:11 2013 +0100 @@ -70,7 +70,7 @@ val prems = Simplifier.prems_of ctxt val ([t'], ctxt') = Variable.import_terms true [t] ctxt val export = singleton (Variable.export ctxt' ctxt) - (* FIXME ctxt cs. ctxt' (!?) *) + (* FIXME ctxt vs. ctxt' (!?) *) val (t1,t2) = Data.dest_bal t' val terms1 = Data.dest_sum t1