src/Pure/sign.ML
changeset 18146 47463b1825c6
parent 18062 7a666583e869
child 18164 eb4206c930cd
     1.1 --- a/src/Pure/sign.ML	Thu Nov 10 20:57:11 2005 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Nov 10 20:57:16 2005 +0100
     1.3 @@ -114,7 +114,7 @@
     1.4    val declared_tyname: theory -> string -> bool
     1.5    val declared_const: theory -> string -> bool
     1.6    val const_monomorphic: theory -> string -> bool
     1.7 -  val const_typargs: theory -> string -> typ -> typ list
     1.8 +  val const_typargs: theory -> string * typ -> typ list
     1.9    val class_space: theory -> NameSpace.T
    1.10    val type_space: theory -> NameSpace.T
    1.11    val const_space: theory -> NameSpace.T
    1.12 @@ -525,7 +525,7 @@
    1.13  
    1.14  fun infer_types_simult pp thy def_type def_sort used freeze args =
    1.15    let
    1.16 -    val termss = foldr multiply [[]] (map fst args);
    1.17 +    val termss = fold_rev (multiply o fst) args [[]];
    1.18      val typs =
    1.19        map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
    1.20