src/Provers/Arith/abel_cancel.ML

    handle Cancel => None;
 
 
  val sum_conv = 
      Simplifier.mk_simproc "cancel_sums"
-       (map (Thm.read_cterm (sign_of Data.thy)) 
+       (map (Thm.read_cterm (Theory.sign_of Data.thy)) 
 	[("x + y", Data.T), ("x - y", Data.T)])
        sum_proc;
 
 
  (*A simproc to cancel like terms on the opposite sides of relations:

    in Some thm end
    handle Cancel => None;
 
  val rel_conv = 
      Simplifier.mk_simproc "cancel_relations"
-       (map (Thm.cterm_of (sign_of Data.thy) o Data.dest_eqI) eqI_rules)
+       (map (Thm.cterm_of (Theory.sign_of Data.thy) o Data.dest_eqI) eqI_rules)
        rel_proc;
 
 end;