# HG changeset patch
# User wenzelm
# Date 1131442988 -3600
# Node ID 61a430a67d7c0e3cc5203247e688f6b3fc1ea31b
# Parent  92c98f31f82da5e9822a7827600478c455766ad1
const args: do not store variable names (unused);

diff -r 92c98f31f82d -r 61a430a67d7c src/Pure/consts.ML
--- a/src/Pure/consts.ML	Tue Nov 08 10:43:05 2005 +0100
+++ b/src/Pure/consts.ML	Tue Nov 08 10:43:08 2005 +0100
@@ -27,10 +27,8 @@
 
 (** datatype T **)
 
-type arg = (indexname * sort) * int list;  (*type variable with first occurrence*)
-
 datatype T = Consts of
- {declarations: ((typ * arg list) * serial) NameSpace.table,
+ {declarations: ((typ * int list list) * serial) NameSpace.table,
   constraints: typ Symtab.table};
 
 fun make_consts (declarations, constraints) =
@@ -68,9 +66,7 @@
   | sub T [] = T
   | sub T _ = raise Subscript;
 
-fun typargs consts c =
-  let val (_, args) = the_const consts c
-  in fn T => map (sub T o #2) args end;
+fun typargs consts c T = map (sub T) (#2 (the_const consts c));
 
 
 
@@ -92,7 +88,7 @@
       | args (TFree _) _ = I
     and args_list (T :: Ts) i is = args T (i :: is) #> args_list Ts (i + 1) is
       | args_list [] _ _ = I;
-  in rev (args declT [] []) end;
+  in map #2 (rev (args declT [] [])) end;
 
 fun declare naming (c, T) = map_consts (apfst (fn declarations =>
   let