equal
deleted
inserted
replaced
735 fun unlam_def ctxt def = |
735 fun unlam_def ctxt def = |
736 let |
736 let |
737 val (lhs, rhs) = Thm.dest_equals (cprop_of def) |
737 val (lhs, rhs) = Thm.dest_equals (cprop_of def) |
738 val xs = strip_abs_vars (term_of rhs) |
738 val xs = strip_abs_vars (term_of rhs) |
739 val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt |
739 val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt |
740 |
740 |
741 fun get_lhs [] = lhs |
741 val thy = ProofContext.theory_of ctxt' |
742 | get_lhs (x::xs) = |
742 fun get_lhs xs = |
743 let val cx = cterm_of (ProofContext.theory_of ctxt') (Free x) |
743 let |
744 in Thm.capply (get_lhs xs) cx end |
744 val cxs = map (cterm_of thy o Free) xs |
|
745 in |
|
746 Drule.list_comb (lhs, cxs) |
|
747 end |
745 |
748 |
746 fun get_conv [] = Conv.rewr_conv def |
749 fun get_conv [] = Conv.rewr_conv def |
747 | get_conv (x::xs) = Conv.fun_conv (get_conv xs) |
750 | get_conv (x::xs) = Conv.fun_conv (get_conv xs) |
748 |
751 |
749 in |
752 in |
750 get_conv xs (get_lhs (rev xs)) |> |
753 get_conv xs (get_lhs xs) |> |
751 singleton (ProofContext.export ctxt' ctxt) |
754 singleton (ProofContext.export ctxt' ctxt) |
752 end |
755 end |
753 *} |
756 *} |
754 |
757 |
755 local_setup {* |
758 local_setup {* |