src/HOL/hologic.ML

--- a/src/HOL/hologic.ML	Sat Feb 02 03:28:36 2008 +0100
+++ b/src/HOL/hologic.ML	Mon Feb 04 10:52:37 2008 +0100
@@ -87,6 +87,7 @@
   val dest_nat: term -> int
   val class_size: string
   val size_const: typ -> term
+  val indexT: typ
   val bitT: typ
   val B0_const: term
   val B1_const: term
@@ -446,6 +447,11 @@
 fun size_const T = Const ("Nat.size_class.size", T --> natT);
 
 
+(* index *)
+
+val indexT = Type ("Code_Index.index", []);
+
+
 (* bit *)
 
 val bitT = Type ("Int.bit", []);