src/Pure/Proof/extraction.ML

                     val (defs'', corr_prf) =
                       corr (d + 1) defs' vs' [] [] [] prf' prf' None;
                     val args = vfs_of prop;
                     val corr_prf' = foldr forall_intr_prf (args, corr_prf);
                   in
-                    ((name, (vs', ((nullt, nullt), corr_prf'))) :: defs',
+                    ((name, (vs', ((nullt, nullt), corr_prf'))) :: defs'',
                      prf_subst_TVars tye' corr_prf')
                   end
               | Some (_, prf') => (defs', prf_subst_TVars tye' prf'))
             | Some rs => (case find vs' rs of
                 Some (_, prf') => (defs', prf_subst_TVars tye' prf')

                                 (chtype [T --> propT] reflexive_axm %> f) %%
                                 PAxm (cname ^ "_def", eqn,
                                   Some (map TVar (term_tvars eqn))))) %%
                             corr_prf)))
                   in
-                    ((s, (vs', ((t', u), corr_prf'))) :: defs',
+                    ((s, (vs', ((t', u), corr_prf'))) :: defs'',
                      subst_TVars tye' u)
                   end
               | Some ((_, u), _) => (defs, subst_TVars tye' u))
             | Some rs => (case find vs' rs of
                 Some (t, _) => (defs, subst_TVars tye' t)