739 val ty = exchange_ty rty qty (fastype_of tm) |
739 val ty = exchange_ty rty qty (fastype_of tm) |
740 in fst (get_fun repF rty qty lthy ty) $ tm end |
740 in fst (get_fun repF rty qty lthy ty) $ tm end |
741 |
741 |
742 fun mk_abs tm = |
742 fun mk_abs tm = |
743 let |
743 let |
744 val _ = tracing (Syntax.string_of_term @{context} tm) |
|
745 val _ = tracing (Syntax.string_of_typ @{context} (fastype_of tm)) |
|
746 val ty = exchange_ty rty qty (fastype_of tm) in |
744 val ty = exchange_ty rty qty (fastype_of tm) in |
747 fst (get_fun absF rty qty lthy ty) $ tm end |
745 fst (get_fun absF rty qty lthy ty) $ tm end |
748 |
746 |
749 fun is_constructor (Const (x, _)) = member (op =) constructors x |
747 fun is_constructor (Const (x, _)) = member (op =) constructors x |
750 | is_constructor _ = false; |
748 | is_constructor _ = false; |
769 end |
767 end |
770 )) |
768 )) |
771 end |
769 end |
772 | x => |
770 | x => |
773 let |
771 let |
774 val _ = tracing (">>" ^ Syntax.string_of_term @{context} tm) |
|
775 val (opp, tms0) = Term.strip_comb tm |
772 val (opp, tms0) = Term.strip_comb tm |
776 val tms = map (build_aux lthy) tms0 |
773 val tms = map (build_aux lthy) tms0 |
777 val ty = fastype_of tm |
774 val ty = fastype_of tm |
778 in |
775 in |
779 if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false) |
776 if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false) |
780 then (list_comb (opp, (hd tms0) :: (tl tms))) |
777 then (list_comb (opp, (hd tms0) :: (tl tms))) |
781 else if (is_constructor opp andalso needs_lift rty ty) then |
778 else if (is_constructor opp andalso needs_lift rty ty) then |
782 mk_rep (mk_abs (list_comb (opp,tms))) |
779 mk_rep (mk_abs (list_comb (opp,tms))) |
783 else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then |
780 else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then |
784 mk_rep(mk_abs(list_comb(opp,tms))) |
781 mk_rep(mk_abs(list_comb(opp,tms))) |
785 else if tms = [] then opp |
782 else if tms = [] then opp |
786 else list_comb(opp, tms) |
783 else list_comb(opp, tms) |
787 end |
784 end |
788 in |
785 in |
789 build_aux lthy (Thm.prop_of thm) |
786 build_aux lthy (Thm.prop_of thm) |