src/Provers/Arith/abel_cancel.ML

--- a/src/Provers/Arith/abel_cancel.ML	Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Thu Jul 08 19:34:56 2004 +0200
@@ -125,7 +125,7 @@
 
  val sum_conv =
      Simplifier.mk_simproc "cancel_sums"
-       (map (Thm.read_cterm (Sign.deref sg_ref))
+       (map (Thm.cterm_fun Logic.varify o Thm.read_cterm (Sign.deref sg_ref))
         [("x + y", Data.T), ("x - y", Data.T)])  (* FIXME depends on concrete syntax !???!!??! *)
        sum_proc;