# HG changeset patch
# User wenzelm
# Date 1264714788 -3600
# Node ID e35f608f81a2e5531c2c434cddf2d055a29e1eb2
# Parent  008126f730a0ab544bcf6cb31b1442a017c9f86f
tuned signature;

diff -r 008126f730a0 -r e35f608f81a2 src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Jan 28 22:38:11 2010 +0100
+++ b/src/Pure/term.ML	Thu Jan 28 22:39:48 2010 +0100
@@ -12,10 +12,10 @@
 
 signature BASIC_TERM =
 sig
-  eqtype indexname
-  eqtype class
-  eqtype sort
-  eqtype arity
+  type indexname = string * int
+  type class = string
+  type sort = class list
+  type arity = string * sort list * sort
   datatype typ =
     Type  of string * typ list |
     TFree of string * sort |