1.1 --- a/src/Tools/misc_legacy.ML	Thu Apr 19 08:45:13 2012 +0200
     1.2 +++ b/src/Tools/misc_legacy.ML	Thu Apr 19 10:16:51 2012 +0200
     1.3 @@ -260,7 +260,7 @@
     1.4       val thy = Thm.theory_of_thm fth
     1.5   in
     1.6     case Thm.fold_terms Term.add_vars fth [] of
     1.7 -       [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
     1.8 +       [] => (fth, fn _ => fn x => x)   (*No vars: nothing to do!*)
     1.9       | vars =>
    1.10           let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
    1.11               val alist = map newName vars