equal
deleted
inserted
replaced
436 fun zip_vars xs ys = |
436 fun zip_vars xs ys = |
437 zip_options xs ys handle ListPair.UnequalLengths => |
437 zip_options xs ys handle ListPair.UnequalLengths => |
438 err "more instantiations than variables in thm"; |
438 err "more instantiations than variables in thm"; |
439 |
439 |
440 val thm' = |
440 val thm' = |
441 Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm; |
441 Thm.instantiate ((zip_vars (build_rev (Thm.fold_terms Term.add_tvars thm)) cTs), []) thm; |
442 val thm'' = |
442 val thm'' = |
443 Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm'; |
443 Thm.instantiate ([], zip_vars (build_rev (Thm.fold_terms Term.add_vars thm')) cts) thm'; |
444 in thm'' end; |
444 in thm'' end; |
445 |
445 |
446 |
446 |
447 (* forall_intr_frees: generalization over all suitable Free variables *) |
447 (* forall_intr_frees: generalization over all suitable Free variables *) |
448 |
448 |
530 |
530 |
531 (* rules *) |
531 (* rules *) |
532 |
532 |
533 fun stripped_sorts thy t = |
533 fun stripped_sorts thy t = |
534 let |
534 let |
535 val tfrees = rev (Term.add_tfrees t []); |
535 val tfrees = build_rev (Term.add_tfrees t); |
536 val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees)); |
536 val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees)); |
537 val recover = |
537 val recover = |
538 map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S)))) |
538 map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S)))) |
539 tfrees' tfrees; |
539 tfrees' tfrees; |
540 val strip = map (apply2 TFree) (tfrees ~~ tfrees'); |
540 val strip = map (apply2 TFree) (tfrees ~~ tfrees'); |