uncurried Consts.typargs;
authorwenzelm
Thu Nov 10 20:57:16 2005 +0100 (2005-11-10)
changeset 1814647463b1825c6
parent 18145 6757627acf59
child 18147 31634a2af39e
uncurried Consts.typargs;
src/Provers/blast.ML
src/Pure/consts.ML
src/Pure/sign.ML
     1.1 --- a/src/Provers/blast.ML	Thu Nov 10 20:57:11 2005 +0100
     1.2 +++ b/src/Provers/blast.ML	Thu Nov 10 20:57:16 2005 +0100
     1.3 @@ -178,13 +178,13 @@
     1.4  		 | SOME v => v)
     1.5  
     1.6  (*refer to the theory in which blast is initialized*)
     1.7 -val typargs = ref (fn (_: string) => fn (T: typ) => [T]);
     1.8 +val typargs = ref (fn ((_, T): string * typ) => [T]);
     1.9  
    1.10  (*Convert a Term.Const to a Blast.Const or Blast.TConst,
    1.11    converting its type to a Blast.term in the latter case.*)
    1.12  fun fromConst alist (a as "all", _) = Const a
    1.13    | fromConst alist (a, T) =
    1.14 -      (case ! typargs a T of
    1.15 +      (case ! typargs (a, T) of
    1.16          [] => Const a
    1.17        | [T] => TConst (a, fromType alist T)
    1.18        | Ts => TConst (a, list_comb (Const "*typargs*", map (fromType alist) Ts)));
     2.1 --- a/src/Pure/consts.ML	Thu Nov 10 20:57:11 2005 +0100
     2.2 +++ b/src/Pure/consts.ML	Thu Nov 10 20:57:16 2005 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4    val declaration: T -> string -> typ  (*exception TYPE*)
     2.5    val constraint: T -> string -> typ    (*exception TYPE*)
     2.6    val monomorphic: T -> string -> bool
     2.7 -  val typargs: T -> string -> typ -> typ list
     2.8 +  val typargs: T -> string * typ -> typ list
     2.9    val declare: NameSpace.naming -> bstring * typ -> T -> T
    2.10    val constrain: string * typ -> T -> T
    2.11    val hide: bool -> string -> T -> T
    2.12 @@ -66,7 +66,7 @@
    2.13    | sub T [] = T
    2.14    | sub T _ = raise Subscript;
    2.15  
    2.16 -fun typargs consts c T = map (sub T) (#2 (the_const consts c));
    2.17 +fun typargs consts (c, T) = map (sub T) (#2 (the_const consts c));
    2.18  
    2.19  
    2.20  
     3.1 --- a/src/Pure/sign.ML	Thu Nov 10 20:57:11 2005 +0100
     3.2 +++ b/src/Pure/sign.ML	Thu Nov 10 20:57:16 2005 +0100
     3.3 @@ -114,7 +114,7 @@
     3.4    val declared_tyname: theory -> string -> bool
     3.5    val declared_const: theory -> string -> bool
     3.6    val const_monomorphic: theory -> string -> bool
     3.7 -  val const_typargs: theory -> string -> typ -> typ list
     3.8 +  val const_typargs: theory -> string * typ -> typ list
     3.9    val class_space: theory -> NameSpace.T
    3.10    val type_space: theory -> NameSpace.T
    3.11    val const_space: theory -> NameSpace.T
    3.12 @@ -525,7 +525,7 @@
    3.13  
    3.14  fun infer_types_simult pp thy def_type def_sort used freeze args =
    3.15    let
    3.16 -    val termss = foldr multiply [[]] (map fst args);
    3.17 +    val termss = fold_rev (multiply o fst) args [[]];
    3.18      val typs =
    3.19        map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
    3.20