# HG changeset patch
# User haftmann
# Date 1455742315 -3600
# Node ID 1cf129590be80ec93bfa233085599654265a77a8
# Parent  a594429637fdf018b1f6582bceb7b55ddef588aa
consolidated name

diff -r a594429637fd -r 1cf129590be8 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Feb 17 21:51:55 2016 +0100
@@ -2442,9 +2442,9 @@
   | num_of_term vs @{term "1::int"} = @{code C} (@{code int_of_integer} 1)
   | num_of_term vs @{term "- 1::int"} = @{code C} (@{code int_of_integer} (~ 1))
   | num_of_term vs (@{term "numeral :: _ \<Rightarrow> int"} $ t) =
-      @{code C} (@{code int_of_integer} (HOLogic.dest_num t))
+      @{code C} (@{code int_of_integer} (HOLogic.dest_numeral t))
   | num_of_term vs (@{term "- numeral :: _ \<Rightarrow> int"} $ t) =
-      @{code C} (@{code int_of_integer} (~(HOLogic.dest_num t)))
+      @{code C} (@{code int_of_integer} (~(HOLogic.dest_numeral t)))
   | num_of_term vs (Bound i) = @{code Bound} (@{code nat_of_integer} i)
   | num_of_term vs (@{term "uminus :: int \<Rightarrow> int"} $ t') = @{code Neg} (num_of_term vs t')
   | num_of_term vs (@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
diff -r a594429637fd -r 1cf129590be8 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Wed Feb 17 21:51:55 2016 +0100
@@ -5547,17 +5547,17 @@
        of @{code C} i => @{code Mul} (i, num_of_term vs t2)
         | _ => error "num_of_term: unsupported Multiplication")
   | num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t')) =
-      mk_C (HOLogic.dest_num t')
+      mk_C (HOLogic.dest_numeral t')
   | num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t')) =
-      mk_C (~ (HOLogic.dest_num t'))
+      mk_C (~ (HOLogic.dest_numeral t'))
   | num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "floor :: real \<Rightarrow> int"} $ t')) =
       @{code Floor} (num_of_term vs t')
   | num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "ceiling :: real \<Rightarrow> int"} $ t')) =
       @{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t')))
   | num_of_term vs (@{term "numeral :: _ \<Rightarrow> real"} $ t') =
-      mk_C (HOLogic.dest_num t')
+      mk_C (HOLogic.dest_numeral t')
   | num_of_term vs (@{term "- numeral :: _ \<Rightarrow> real"} $ t') =
-      mk_C (~ (HOLogic.dest_num t'))
+      mk_C (~ (HOLogic.dest_numeral t'))
   | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
 
 fun fm_of_term vs @{term True} = @{code T}
@@ -5569,9 +5569,9 @@
   | fm_of_term vs (@{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
   | fm_of_term vs (@{term "op rdvd"} $ (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
-      mk_Dvd (HOLogic.dest_num t1, num_of_term vs t2)
+      mk_Dvd (HOLogic.dest_numeral t1, num_of_term vs t2)
   | fm_of_term vs (@{term "op rdvd"} $ (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
-      mk_Dvd (~ (HOLogic.dest_num t1), num_of_term vs t2)
+      mk_Dvd (~ (HOLogic.dest_numeral t1), num_of_term vs t2)
   | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) =
diff -r a594429637fd -r 1cf129590be8 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 17 21:51:55 2016 +0100
@@ -1672,7 +1672,7 @@
     fun do_numeral depth Ts mult T some_t0 t1 t2 =
       (if is_number_type ctxt T then
          let
-           val j = mult * HOLogic.dest_num t2
+           val j = mult * HOLogic.dest_numeral t2
          in
            if j = 1 then
              raise SAME ()
diff -r a594429637fd -r 1cf129590be8 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/Tools/hologic.ML	Wed Feb 17 21:51:55 2016 +0100
@@ -100,7 +100,7 @@
   val mk_bit: int -> term
   val dest_bit: term -> int
   val mk_numeral: int -> term
-  val dest_num: term -> int
+  val dest_numeral: term -> int
   val numeral_const: typ -> term
   val add_numerals: term -> (term * typ) list -> (term * typ) list
   val mk_number: typ -> int -> term
@@ -533,10 +533,10 @@
   in if i > 0 then mk i else raise TERM ("mk_numeral: " ^ string_of_int i, [])
   end
 
-fun dest_num (Const ("Num.num.One", _)) = 1
-  | dest_num (Const ("Num.num.Bit0", _) $ bs) = 2 * dest_num bs
-  | dest_num (Const ("Num.num.Bit1", _) $ bs) = 2 * dest_num bs + 1
-  | dest_num t = raise TERM ("dest_num", [t]);
+fun dest_numeral (Const ("Num.num.One", _)) = 1
+  | dest_numeral (Const ("Num.num.Bit0", _) $ bs) = 2 * dest_numeral bs
+  | dest_numeral (Const ("Num.num.Bit1", _) $ bs) = 2 * dest_numeral bs + 1
+  | dest_numeral t = raise TERM ("dest_num", [t]);
 
 fun numeral_const T = Const ("Num.numeral_class.numeral", numT --> T);
 
@@ -554,7 +554,7 @@
 fun dest_number (Const ("Groups.zero_class.zero", T)) = (T, 0)
   | dest_number (Const ("Groups.one_class.one", T)) = (T, 1)
   | dest_number (Const ("Num.numeral_class.numeral", Type ("fun", [_, T])) $ t) =
-      (T, dest_num t)
+      (T, dest_numeral t)
   | dest_number (Const ("Groups.uminus_class.uminus", Type ("fun", [_, T])) $ t) =
       apsnd (op ~) (dest_number t)
   | dest_number t = raise TERM ("dest_number", [t]);
diff -r a594429637fd -r 1cf129590be8 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Wed Feb 17 21:51:55 2016 +0100
@@ -175,11 +175,11 @@
     | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, Rat.zero)
     | demult (Const (@{const_name Groups.one}, _), m) = (NONE, m)
     (*Warning: in rare cases (neg_)numeral encloses a non-numeral,
-      in which case dest_num raises TERM; hence all the handles below.
+      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 ("Num.numeral_class.numeral", _) $ n, m) =
-      ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_num n)))
+      ((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)))
@@ -208,7 +208,7 @@
     | poly (Const (@{const_name Groups.one}, _), m, (p, i)) =
         (p, Rat.add i m)
     | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
-        (let val k = HOLogic.dest_num t
+        (let val k = HOLogic.dest_numeral t
         in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k))) end
         handle TERM _ => add_atom all m pi)
     | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =