# HG changeset patch
# User wenzelm
# Date 1131652636 -3600
# Node ID 47463b1825c67b030d4c7cae0994fbb9713ee551
# Parent  6757627acf593817dcffbe682e5f15efe67ca17c
uncurried Consts.typargs;

diff -r 6757627acf59 -r 47463b1825c6 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Thu Nov 10 20:57:11 2005 +0100
+++ b/src/Provers/blast.ML	Thu Nov 10 20:57:16 2005 +0100
@@ -178,13 +178,13 @@
 		 | SOME v => v)
 
 (*refer to the theory in which blast is initialized*)
-val typargs = ref (fn (_: string) => fn (T: typ) => [T]);
+val typargs = ref (fn ((_, T): string * typ) => [T]);
 
 (*Convert a Term.Const to a Blast.Const or Blast.TConst,
   converting its type to a Blast.term in the latter case.*)
 fun fromConst alist (a as "all", _) = Const a
   | fromConst alist (a, T) =
-      (case ! typargs a T of
+      (case ! typargs (a, T) of
         [] => Const a
       | [T] => TConst (a, fromType alist T)
       | Ts => TConst (a, list_comb (Const "*typargs*", map (fromType alist) Ts)));
diff -r 6757627acf59 -r 47463b1825c6 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Thu Nov 10 20:57:11 2005 +0100
+++ b/src/Pure/consts.ML	Thu Nov 10 20:57:16 2005 +0100
@@ -13,7 +13,7 @@
   val declaration: T -> string -> typ  (*exception TYPE*)
   val constraint: T -> string -> typ    (*exception TYPE*)
   val monomorphic: T -> string -> bool
-  val typargs: T -> string -> typ -> typ list
+  val typargs: T -> string * typ -> typ list
   val declare: NameSpace.naming -> bstring * typ -> T -> T
   val constrain: string * typ -> T -> T
   val hide: bool -> string -> T -> T
@@ -66,7 +66,7 @@
   | sub T [] = T
   | sub T _ = raise Subscript;
 
-fun typargs consts c T = map (sub T) (#2 (the_const consts c));
+fun typargs consts (c, T) = map (sub T) (#2 (the_const consts c));
 
 
 
diff -r 6757627acf59 -r 47463b1825c6 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Nov 10 20:57:11 2005 +0100
+++ b/src/Pure/sign.ML	Thu Nov 10 20:57:16 2005 +0100
@@ -114,7 +114,7 @@
   val declared_tyname: theory -> string -> bool
   val declared_const: theory -> string -> bool
   val const_monomorphic: theory -> string -> bool
-  val const_typargs: theory -> string -> typ -> typ list
+  val const_typargs: theory -> string * typ -> typ list
   val class_space: theory -> NameSpace.T
   val type_space: theory -> NameSpace.T
   val const_space: theory -> NameSpace.T
@@ -525,7 +525,7 @@
 
 fun infer_types_simult pp thy def_type def_sort used freeze args =
   let
-    val termss = foldr multiply [[]] (map fst args);
+    val termss = fold_rev (multiply o fst) args [[]];
     val typs =
       map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;