# HG changeset patch
# User haftmann
# Date 1172846602 -3600
# Node ID 56861fe9c22c71629c3b84b527f44a90322f1ebf
# Parent  378f34b1e38095ed930736adb8a8fa8b8c4a5acc
added add_numerals_of

diff -r 378f34b1e380 -r 56861fe9c22c src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Fri Mar 02 15:43:21 2007 +0100
+++ b/src/HOL/hologic.ML	Fri Mar 02 15:43:22 2007 +0100
@@ -85,6 +85,7 @@
   val mk_numeral: IntInf.int -> term
   val dest_numeral: term -> IntInf.int
   val number_of_const: typ -> term
+  val add_numerals_of: term -> (term * typ) list -> (term * typ) list
   val mk_number: typ -> IntInf.int -> term
   val dest_number: term -> typ * IntInf.int
   val realT: typ
@@ -338,6 +339,22 @@
 
 fun number_of_const T = Const ("Numeral.number_of", intT --> T);
 
+fun add_numerals_of (Const _) =
+      I
+  | add_numerals_of (Var _) =
+      I
+  | add_numerals_of (Free _) =
+      I
+  | add_numerals_of (Bound _) =
+      I
+  | add_numerals_of (Abs (_, _, t)) =
+      add_numerals_of t
+  | add_numerals_of (t as _ $ _) =
+      case strip_comb t
+       of (Const ("Numeral.number_of",
+           Type (_, [_, T])), ts) => fold (cons o rpair T) ts
+        | (t', ts) => add_numerals_of t' #> fold add_numerals_of ts;
+
 fun mk_number T 0 = Const ("HOL.zero", T)
   | mk_number T 1 = Const ("HOL.one", T)
   | mk_number T i = number_of_const T $ mk_numeral i;