| changeset 20713 | 823967ef47f1 |
| parent 20055 | 24c127b97ab5 |
| child 22997 | d4f3b015b50b |
--- a/src/Provers/Arith/abel_cancel.ML Tue Sep 26 13:34:15 2006 +0200 +++ b/src/Provers/Arith/abel_cancel.ML Tue Sep 26 13:34:16 2006 +0200 @@ -28,7 +28,7 @@ (* FIXME dependent on abstract syntax *) -fun zero t = Const ("0", t); +fun zero t = Const ("HOL.zero", t); fun minus t = Const ("HOL.uminus", t --> t); fun add_terms pos (Const ("HOL.plus", _) $ x $ y, ts) =