equal
deleted
inserted
replaced
48 let |
48 let |
49 fun eta_expand thm = |
49 fun eta_expand thm = |
50 let |
50 let |
51 val lhs = (fst o Logic.dest_equals o Drule.plain_prop_of) thm; |
51 val lhs = (fst o Logic.dest_equals o Drule.plain_prop_of) thm; |
52 val tys = (fst o strip_type o fastype_of) lhs; |
52 val tys = (fst o strip_type o fastype_of) lhs; |
|
53 val ctxt = Name.make_context (map (fst o fst) (Term.add_vars lhs [])); |
53 val vs_ct = map (fn (v, ty) => cterm_of thy (Var ((v, 0), ty))) |
54 val vs_ct = map (fn (v, ty) => cterm_of thy (Var ((v, 0), ty))) |
54 (Name.names Name.context "a" tys); |
55 (Name.names ctxt "a" tys); |
55 in |
56 in |
56 fold (fn ct => fn thm => Thm.combination thm (Thm.reflexive ct)) vs_ct thm |
57 fold (fn ct => fn thm => Thm.combination thm (Thm.reflexive ct)) vs_ct thm |
57 end; |
58 end; |
58 fun beta_norm thm = |
59 fun beta_norm thm = |
59 let |
60 let |