# HG changeset patch
# User blanchet
# Date 1285940756 -7200
# Node ID bb43fe4fac9342beb26c1b6c7e46a9eac43cf8e4
# Parent  75d792edf634092a8e2c40a463ef9381cec928b3
avoid dependency on "int"

diff -r 75d792edf634 -r bb43fe4fac93 src/HOL/Tools/Sledgehammer/meson_clausify.ML
--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 15:34:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 15:45:56 2010 +0200
@@ -351,7 +351,7 @@
     fun intr_imp ct th =
       Thm.instantiate ([], map (pairself (cterm_of @{theory}))
                                [(Var (("i", 1), @{typ nat}),
-                                 HOLogic.mk_number @{typ nat} ax_no)])
+                                 HOLogic.mk_nat ax_no)])
                       @{thm skolem_COMBK_D}
       RS Thm.implies_intr ct th
   in
diff -r 75d792edf634 -r bb43fe4fac93 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Oct 01 15:34:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Oct 01 15:45:56 2010 +0200
@@ -151,7 +151,7 @@
       fun subst_info_for_prem assm_no prem =
         case prem of
           _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) =>
-          let val ax_no = num |> HOLogic.dest_number |> snd in
+          let val ax_no = HOLogic.dest_nat num in
             (ax_no, (assm_no, match_term (nth axioms ax_no |> snd, t)))
           end
         | _ => raise TERM ("discharge_skolem_premises: Malformed premise",