59 val vars = raw_vars @ map (Thm.term_of o snd) params; |
59 val vars = raw_vars @ map (Thm.term_of o snd) params; |
60 val names_ctxt = ctxt |
60 val names_ctxt = ctxt |
61 |> fold Variable.declare_names vars |
61 |> fold Variable.declare_names vars |
62 |> fold Variable.declare_thm (raw_thm :: prems); |
62 |> fold Variable.declare_thm (raw_thm :: prems); |
63 val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl; |
63 val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl; |
64 val (rhoTs, rhots) = Thm.match (thm_concl, concl) |
64 val (instT, inst) = Thm.match (thm_concl, concl); |
65 |>> map (apply2 Thm.typ_of) |
65 val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT; |
66 ||> map (apply2 Thm.term_of); |
66 val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst; |
67 val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd |
67 val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd |
68 |> map (subst_atomic_types rhoTs); |
68 |> map (subst_atomic_types rhoTs); |
69 val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs; |
69 val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs; |
70 val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs |
70 val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs |
71 |>> (fn names => Variable.variant_fixes names names_ctxt) ; |
71 |>> (fn names => Variable.variant_fixes names names_ctxt) ; |