src/Pure/Proof/extraction.ML

             val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye;
             val T = etype_of sg vs' [] prop;
             val defs' = if T = nullT then defs
               else fst (extr d defs vs ts Ts hs prf0)
           in
-            if T = nullT andalso realizes_null vs' prop = prop then (defs, prf0)
+            if T = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0)
             else case Symtab.lookup (realizers, name) of
               None => (case find vs' (find' name defs') of
                 None =>
                   let
                     val _ = assert (T = nullT) "corr: internal error";

       | corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, Some Ts')) _ _ =
           let
             val (vs', tye) = find_inst prop Ts ts vs;
             val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
           in
-            case find vs' (Symtab.lookup_multi (realizers, s)) of
+            if etype_of sg vs' [] prop = nullT andalso
+              realizes_null vs' prop aconv prop then (defs, prf0)
+            else case find vs' (Symtab.lookup_multi (realizers, s)) of
               Some (_, prf) => (defs, prf_subst_TVars tye' prf)
             | None => error ("corr: no realizer for instance of axiom " ^
                 quote s ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
                   (Reconstruct.prop_of (proof_combt (prf0, ts)))))
           end

             val (vs', tye) = find_inst prop Ts ts vs;
             val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
           in
             case find vs' (Symtab.lookup_multi (realizers, s)) of
               Some (t, _) => (defs, subst_TVars tye' t)
-            | None => error ("no realizer for instance of axiom " ^
+            | None => error ("extr: no realizer for instance of axiom " ^
                 quote s ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
                   (Reconstruct.prop_of (proof_combt (prf0, ts)))))
           end
 
       | extr d defs vs ts Ts hs _ = error "extr: bad proof";