Moved cterm_fun from Thm to Drule.

--- 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;