# HG changeset patch
# User wenzelm
# Date 1119298438 -7200
# Node ID 77ae3bfa8b76021439179437c24b7f3af2055e4e
# Parent  eaf7bb77fed690f2d9ee935f71d9a71fc0041cef
get_thm instead of obsolete Goals.get_thm;
improved msg;

diff -r eaf7bb77fed6 -r 77ae3bfa8b76 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Mon Jun 20 22:13:57 2005 +0200
+++ b/src/HOL/arith_data.ML	Mon Jun 20 22:13:58 2005 +0200
@@ -423,7 +423,7 @@
     inj_thms = inj_thms,
     lessD = lessD @ [Suc_leI],
     neqE = [linorder_neqE_nat,
-      Goals.get_thm (theory "Ring_and_Field") "linorder_neqE_ordered_idom"],
+      get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
     simpset = HOL_basic_ss addsimps add_rules
                    addsimprocs [ab_group_add_cancel.sum_conv, 
                                 ab_group_add_cancel.rel_conv]
@@ -464,7 +464,7 @@
 fun presburger_tac i st =
   (case ArithTheoryData.get (sign_of_thm st) of
      {presburger = SOME tac, ...} =>
-       (tracing "Simple arithmetic decision procedure failed.\nNow trying full Presburger arithmetic..."; tac i st)
+       (warning "Simple arithmetic decision procedure failed, trying full Presburger arithmetic..."; tac i st)
    | _ => no_tac st);
 
 in