1.1 --- a/src/Pure/term.ML	Thu Mar 05 15:27:07 2009 +0100
     1.2 +++ b/src/Pure/term.ML	Thu Mar 05 17:09:07 2009 +0100
     1.3 @@ -805,8 +805,8 @@
     1.4  fun close_schematic_term t =
     1.5    let
     1.6      val extra_types = map (fn v => Const ("TYPE", itselfT (TVar v))) (hidden_polymorphism t);
     1.7 -    val extra_terms = map Var (rev (add_vars t []));
     1.8 -  in fold_rev lambda (extra_types @ extra_terms) t end;
     1.9 +    val extra_terms = map Var (add_vars t []);
    1.10 +  in fold lambda (extra_terms @ extra_types) t end;
    1.11  
    1.12  
    1.13