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