# HG changeset patch
# User paulson
# Date 956482796 -7200
# Node ID 9f18aba48519b43132023f6efe49deb7c9681b06
# Parent  eae30939b5925c5d6429dc349ad1cfa4535e2ef9
number_of now takes a type arg

diff -r eae30939b592 -r 9f18aba48519 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Sun Apr 23 11:39:32 2000 +0200
+++ b/src/HOL/hologic.ML	Sun Apr 23 11:39:56 2000 +0200
@@ -66,7 +66,7 @@
   val pls_const: term
   val min_const: term
   val bit_const: term
-  val number_of_const: term
+  val number_of_const: typ -> term
   val int_of: int list -> int
   val dest_binum: term -> int
 end;
@@ -246,8 +246,9 @@
 
 val pls_const =  Const ("Numeral.bin.Pls", binT)
 and min_const = Const ("Numeral.bin.Min", binT)
-and bit_const = Const ("Numeral.bin.Bit", [binT, boolT] ---> binT)
-and number_of_const = Const ("Numeral.number_of", binT --> natT);
+and bit_const = Const ("Numeral.bin.Bit", [binT, boolT] ---> binT);
+
+fun number_of_const T = Const ("Numeral.number_of", binT --> T);
 
 
 fun int_of [] = 0