src/Pure/thm.ML

         val thy' = Context.certificate_theory cert handle ERROR msg =>
           raise CONTEXT (msg, [], [], [state, orule], Option.map Context.Proof opt_ctxt);
         val constraints' =
           union_constraints constraints1 constraints2
           |> insert_constraints_env thy' env;
-        fun zproof p q = ZTerm.todo_proof p;
+        fun zproof p q =
+          ZTerm.bicompose_proof thy' env smax flatten Bs As A oldAs n (nlift + 1) p q;
         fun proof p q =
           Proofterm.bicompose_proof env smax flatten Bs As A oldAs n (nlift + 1) p q;
         val th =
           Thm (deriv_rule2 zproof proof rder' sder,
            {tags = [],