src/HOL/Tools/lin_arith.ML

     | demult (Const (@{const_name HOL.one}, _), m) = (NONE, m)
     (*Warning: in rare cases number_of encloses a non-numeral,
       in which case dest_numeral raises TERM; hence all the handles below.
       Same for Suc-terms that turn out not to be numerals -
       although the simplifier should eliminate those anyway ...*)
-    | demult (t as Const ("Numeral.number_class.number_of", _) $ n, m) =
+    | demult (t as Const ("Int.number_class.number_of", _) $ n, m) =
       ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n)))
         handle TERM _ => (SOME t, m))
     | demult (t as Const (@{const_name Suc}, _) $ _, m) =
       ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_nat t)))
         handle TERM _ => (SOME t, m))

          | (SOME u, m') => add_atom u m' pi)
     | poly (all as Const (@{const_name HOL.divide}, _) $ _ $ _, m, pi as (p, i)) =
         (case demult inj_consts (all, m) of
            (NONE,   m') => (p, Rat.add i m')
          | (SOME u, m') => add_atom u m' pi)
-    | poly (all as Const ("Numeral.number_class.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
+    | poly (all as Const ("Int.number_class.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
         (let val k = HOLogic.dest_numeral t
             val k2 = if k < 0 andalso T = HOLogic.natT then 0 else k
         in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k2))) end
         handle TERM _ => add_atom all m pi)
     | poly (all as Const f $ x, m, pi) =

     case head_of lhs of
       Const (a, _) => member (op =) [@{const_name Orderings.max},
                                     @{const_name Orderings.min},
                                     @{const_name HOL.abs},
                                     @{const_name HOL.minus},
-                                    "IntDef.nat",
+                                    "Int.nat",
                                     "Divides.div_class.mod",
                                     "Divides.div_class.div"] a
     | _            => (warning ("Lin. Arith.: wrong format for split rule " ^
                                  Display.string_of_thm thm);
                        false))

         val subgoal2        = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false]
       in
         SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)]
       end
     (* ?P (nat ?i) = ((ALL n. ?i = int n --> ?P n) & (?i < 0 --> ?P 0)) *)
-    | (Const ("IntDef.nat", _), [t1]) =>
+    | (Const ("Int.nat", _), [t1]) =>
       let
         val rev_terms   = rev terms
         val zero_int    = Const (@{const_name HOL.zero}, HOLogic.intT)
         val zero_nat    = Const (@{const_name HOL.zero}, HOLogic.natT)
         val n           = Bound 0

           (neg (number_of (uminus ?k)) -->
             (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
           (neg (number_of ?k) -->
             (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
     | (Const ("Divides.div_class.mod",
-        Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+        Type ("fun", [Type ("Int.int", []), _])), [t1, t2 as (number_of $ k)]) =>
       let
         val rev_terms               = rev terms
         val zero                    = Const (@{const_name HOL.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
         val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, j)])
                                         (map (incr_boundvars 2) rev_terms)
         val t1'                     = incr_boundvars 2 t1
         val (t2' as (_ $ k'))       = incr_boundvars 2 t2
-        val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
-        val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
+        val iszero_t2               = Const ("Int.iszero", split_type --> HOLogic.boolT) $ t2
+        val neg_minus_k             = Const ("Int.neg", split_type --> HOLogic.boolT) $
                                         (number_of $
                                           (Const (@{const_name HOL.uminus},
                                             HOLogic.intT --> HOLogic.intT) $ k'))
         val zero_leq_j              = Const (@{const_name HOL.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j

                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
                                          (Const (@{const_name HOL.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
-        val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
+        val neg_t2                  = Const ("Int.neg", split_type --> HOLogic.boolT) $ t2'
         val t2_lt_j                 = Const (@{const_name HOL.less},
                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
         val j_leq_zero              = Const (@{const_name HOL.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)

           (neg (number_of (uminus ?k)) -->
             (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
           (neg (number_of ?k) -->
             (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
     | (Const ("Divides.div_class.div",
-        Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+        Type ("fun", [Type ("Int.int", []), _])), [t1, t2 as (number_of $ k)]) =>
       let
         val rev_terms               = rev terms
         val zero                    = Const (@{const_name HOL.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
         val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, i)])
                                         (map (incr_boundvars 2) rev_terms)
         val t1'                     = incr_boundvars 2 t1
         val (t2' as (_ $ k'))       = incr_boundvars 2 t2
-        val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
-        val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
+        val iszero_t2               = Const ("Int.iszero", split_type --> HOLogic.boolT) $ t2
+        val neg_minus_k             = Const ("Int.neg", split_type --> HOLogic.boolT) $
                                         (number_of $
                                           (Const (@{const_name HOL.uminus},
                                             HOLogic.intT --> HOLogic.intT) $ k'))
         val zero_leq_j              = Const (@{const_name HOL.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j

         val t1_eq_t2_times_i_plus_j = Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
                                          (Const (@{const_name HOL.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
-        val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
+        val neg_t2                  = Const ("Int.neg", split_type --> HOLogic.boolT) $ t2'
         val t2_lt_j                 = Const (@{const_name HOL.less},
                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
         val j_leq_zero              = Const (@{const_name HOL.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)