src/HOL/hologic.ML

   val Suc_zero: term
   val mk_nat: int -> term
   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
   val mk_bit: int -> term
   val dest_bit: term -> int

 val class_size = "Nat.size";
 
 fun size_const T = Const ("Nat.size_class.size", T --> natT);
 
 
+(* index *)
+
+val indexT = Type ("Code_Index.index", []);
+
+
 (* bit *)
 
 val bitT = Type ("Int.bit", []);
 
 val B0_const = Const ("Int.bit.B0", bitT);