Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Provers/Arith/abel_cancel.ML
changeset 35845 e5980f0ad025
parent 35762 af3ff2ba4c54 
--- a/src/Provers/Arith/abel_cancel.ML	Sat Mar 20 02:23:41 2010 +0100
+++ b/src/Provers/Arith/abel_cancel.ML	Sat Mar 20 17:33:11 2010 +0100
@@ -88,7 +88,7 @@
 
 val sum_conv =
   Simplifier.mk_simproc "cancel_sums"
-    (map (Drule.cterm_fun Logic.varify) Data.sum_pats) (K sum_proc);
+    (map (Drule.cterm_fun Logic.varify_global) Data.sum_pats) (K sum_proc);
 
 
 (*A simproc to cancel like terms on the opposite sides of relations:
isabelle