# HG changeset patch
# User haftmann
# Date 1202118757 -3600
# Node ID f9e779f119491ccf5ac03cecf3c384b6a36c5bc9
# Parent  9f8810c42604fa4a9a6b24e6ab7fe4d2f215edf2
added indexT

diff -r 9f8810c42604 -r f9e779f11949 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", []);