# HG changeset patch
# User haftmann
# Date 1236877287 -3600
# Node ID 55f2933bef6eeec94b882c2077b51c15604deade
# Parent  45b434d8ef8dade1815716dc8b8ecfca1c2fdf35
tuned

diff -r 45b434d8ef8d -r 55f2933bef6e src/HOL/Tools/rat_arith.ML
--- a/src/HOL/Tools/rat_arith.ML	Thu Mar 12 18:01:26 2009 +0100
+++ b/src/HOL/Tools/rat_arith.ML	Thu Mar 12 18:01:27 2009 +0100
@@ -34,8 +34,6 @@
 
 in
 
-val ratT = Type ("Rational.rat", [])
-
 val rat_arith_setup =
   LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
@@ -45,7 +43,7 @@
     neqE =  neqE,
     simpset = simpset addsimps simps
                       addsimprocs simprocs}) #>
-  arith_inj_const (@{const_name of_nat}, HOLogic.natT --> ratT) #>
-  arith_inj_const (@{const_name of_int}, HOLogic.intT --> ratT)
+  arith_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #>
+  arith_inj_const (@{const_name of_int}, @{typ "int => rat"})
 
 end;