equal
deleted
inserted
replaced
258 fun freeze_thaw_robust th = |
258 fun freeze_thaw_robust th = |
259 let val fth = Thm.legacy_freezeT th |
259 let val fth = Thm.legacy_freezeT th |
260 val thy = Thm.theory_of_thm fth |
260 val thy = Thm.theory_of_thm fth |
261 in |
261 in |
262 case Thm.fold_terms Term.add_vars fth [] of |
262 case Thm.fold_terms Term.add_vars fth [] of |
263 [] => (fth, fn i => fn x => x) (*No vars: nothing to do!*) |
263 [] => (fth, fn _ => fn x => x) (*No vars: nothing to do!*) |
264 | vars => |
264 | vars => |
265 let fun newName (ix,_) = (ix, gensym (string_of_indexname ix)) |
265 let fun newName (ix,_) = (ix, gensym (string_of_indexname ix)) |
266 val alist = map newName vars |
266 val alist = map newName vars |
267 fun mk_inst (v,T) = |
267 fun mk_inst (v,T) = |
268 (cterm_of thy (Var(v,T)), |
268 (cterm_of thy (Var(v,T)), |