author | wenzelm |
Sat, 23 Nov 2013 17:07:11 +0100 | |
changeset 54565 | 63e4474fd0ed |
parent 54564 | 5df6e746ad03 |
child 54566 | 5f3e9baa8f13 |
--- 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