src/Tools/misc_legacy.ML
changeset 47576 b32aae03e3d6
parent 47022 8eac39af4ec0
child 51429 48eb29821bd9
--- a/src/Tools/misc_legacy.ML	Thu Apr 19 08:45:13 2012 +0200
+++ b/src/Tools/misc_legacy.ML	Thu Apr 19 10:16:51 2012 +0200
@@ -260,7 +260,7 @@
      val thy = Thm.theory_of_thm fth
  in
    case Thm.fold_terms Term.add_vars fth [] of
-       [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
+       [] => (fth, fn _ => fn x => x)   (*No vars: nothing to do!*)
      | vars =>
          let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
              val alist = map newName vars