Changes

Changeset 64981:ea6199b23dfa by wenzelm:
proper background certificate from make_context, which can be a super-theory of the direct join (amending d07464875dd4);