equal
deleted
inserted
replaced
538 |
538 |
539 val cert = cterm_of (ProofContext.theory_of lthy) |
539 val cert = cterm_of (ProofContext.theory_of lthy) |
540 fun requantify orig_intro thm = |
540 fun requantify orig_intro thm = |
541 let |
541 let |
542 val (qs, t) = dest_all_all orig_intro |
542 val (qs, t) = dest_all_all orig_intro |
543 val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T) |
543 val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T) |
544 val vars = Term.add_vars (prop_of thm) [] |> rev |
544 val vars = Term.add_vars (prop_of thm) [] |
545 val varmap = AList.lookup (op =) (frees ~~ map fst vars) |
545 val varmap = AList.lookup (op =) (frees ~~ map fst vars) |
546 #> the_default ("",0) |
546 #> the_default ("",0) |
547 in |
547 in |
548 fold_rev (fn Free (n, T) => |
548 fold_rev (fn Free (n, T) => |
549 forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm |
549 forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm |
550 end |
550 end |
551 in |
551 in |