src/Pure/consts.ML
changeset 74291 b83fa8f3a271
parent 74266 612b7e0d6721
child 77970 31ea5c1f874d
--- a/src/Pure/consts.ML	Sat Sep 11 13:04:32 2021 +0200
+++ b/src/Pure/consts.ML	Sat Sep 11 21:16:23 2021 +0200
@@ -19,6 +19,7 @@
   val the_const: T -> string -> string * typ                   (*exception TYPE*)
   val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
   val type_scheme: T -> string -> typ                          (*exception TYPE*)
+  val type_arguments: T -> string -> int list list             (*exception TYPE*)
   val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
   val the_constraint: T -> string -> typ                       (*exception TYPE*)
   val space_of: T -> Name_Space.T