get_thm instead of obsolete Goals.get_thm;
authorwenzelm
Mon Jun 20 22:13:58 2005 +0200 (2005-06-20)
changeset 1648577ae3bfa8b76
parent 16484 eaf7bb77fed6
child 16486 1a12cdb6ee6b
get_thm instead of obsolete Goals.get_thm;
improved msg;
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/arith_data.ML	Mon Jun 20 22:13:57 2005 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Mon Jun 20 22:13:58 2005 +0200
     1.3 @@ -423,7 +423,7 @@
     1.4      inj_thms = inj_thms,
     1.5      lessD = lessD @ [Suc_leI],
     1.6      neqE = [linorder_neqE_nat,
     1.7 -      Goals.get_thm (theory "Ring_and_Field") "linorder_neqE_ordered_idom"],
     1.8 +      get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
     1.9      simpset = HOL_basic_ss addsimps add_rules
    1.10                     addsimprocs [ab_group_add_cancel.sum_conv, 
    1.11                                  ab_group_add_cancel.rel_conv]
    1.12 @@ -464,7 +464,7 @@
    1.13  fun presburger_tac i st =
    1.14    (case ArithTheoryData.get (sign_of_thm st) of
    1.15       {presburger = SOME tac, ...} =>
    1.16 -       (tracing "Simple arithmetic decision procedure failed.\nNow trying full Presburger arithmetic..."; tac i st)
    1.17 +       (warning "Simple arithmetic decision procedure failed, trying full Presburger arithmetic..."; tac i st)
    1.18     | _ => no_tac st);
    1.19  
    1.20  in