equal
deleted
inserted
replaced
608 fun join_transfer thy th = |
608 fun join_transfer thy th = |
609 if Context.subthy_id (Context.theory_id thy, theory_id th) then th |
609 if Context.subthy_id (Context.theory_id thy, theory_id th) then th |
610 else transfer thy th; |
610 else transfer thy th; |
611 |
611 |
612 fun join_transfer_context (ctxt, th) = |
612 fun join_transfer_context (ctxt, th) = |
613 if Context.subthy_id (Context.theory_id (Proof_Context.theory_of ctxt), theory_id th) then |
613 if Context.subthy_id (theory_id th, Context.theory_id (Proof_Context.theory_of ctxt)) |
614 (Context.raw_transfer (theory_of_thm th) ctxt, th) |
614 then (ctxt, transfer' ctxt th) |
615 else (ctxt, transfer' ctxt th); |
615 else (Context.raw_transfer (theory_of_thm th) ctxt, th); |
616 |
616 |
617 |
617 |
618 (* matching *) |
618 (* matching *) |
619 |
619 |
620 local |
620 local |