# HG changeset patch
# User huffman
# Date 1181678380 -7200
# Node ID 1517207ec8b9de5f704ecbc65d6e101d1e2bf133
# Parent  b8139ba0c940ca8c4d85bfac7b4a14bf5f509e67
thm antiquotations

diff -r b8139ba0c940 -r 1517207ec8b9 src/HOL/Real/ferrante_rackoff.ML
--- a/src/HOL/Real/ferrante_rackoff.ML	Tue Jun 12 20:49:56 2007 +0200
+++ b/src/HOL/Real/ferrante_rackoff.ML	Tue Jun 12 21:59:40 2007 +0200
@@ -51,7 +51,7 @@
 val context_ss = simpset_of (the_context ());
 
 fun ferrack_tac q i =  ObjectLogic.atomize_tac i
-  THEN REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, abs_split] i)
+  THEN REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}] i)
   THEN (fn st =>
   let
     val g = nth (prems_of st) (i - 1)
@@ -61,7 +61,7 @@
     (* Some simpsets for dealing with mod div abs and nat*)
     val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [@{thm split_min}, @{thm split_max}]
     (* simp rules for elimination of abs *)
-    val simpset3 = HOL_basic_ss addsplits [abs_split]
+    val simpset3 = HOL_basic_ss addsplits [@{thm abs_split}]
     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
     (* Theorem for the nat --> int transformation *)
     val pre_thm = Seq.hd (EVERY
diff -r b8139ba0c940 -r 1517207ec8b9 src/HOL/Real/rat_arith.ML
--- a/src/HOL/Real/rat_arith.ML	Tue Jun 12 20:49:56 2007 +0200
+++ b/src/HOL/Real/rat_arith.ML	Tue Jun 12 21:59:40 2007 +0200
@@ -17,7 +17,8 @@
              @{thm divide_1}, @{thm divide_zero_left},
              @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
              @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
-             of_int_0, of_int_1, @{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff},
+             @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
+             @{thm of_int_minus}, @{thm of_int_diff},
              @{thm of_int_mult}, @{thm of_int_of_nat_eq}]
 
 val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2,