# HG changeset patch
# User berghofe
# Date 1114102974 -7200
# Node ID 348ce23d2fc2d2c5a2918fd3d3f4bb92d5782968
# Parent  997884600e0a78889c1d812a10027ddf6a859769
Moved cterm_fun from Thm to Drule.

diff -r 997884600e0a -r 348ce23d2fc2 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Thu Apr 21 18:58:44 2005 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Thu Apr 21 19:02:54 2005 +0200
@@ -125,7 +125,7 @@
 
  val sum_conv =
      Simplifier.mk_simproc "cancel_sums"
-       (map (Thm.cterm_fun Logic.varify o Thm.read_cterm (Sign.deref sg_ref))
+       (map (Drule.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;