# HG changeset patch
# User berghofe
# Date 1033396966 -7200
# Node ID 73c3915553b4e20d32725319657c9303f3bf6af5
# Parent  9a6f43b8eae1fa9fb869505bc0ba8a9b59235c3f
Added check for axioms with "realizes Null A = A".

diff -r 9a6f43b8eae1 -r 73c3915553b4 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Sep 30 16:40:57 2002 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Sep 30 16:42:46 2002 +0200
@@ -445,7 +445,7 @@
             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 =>
@@ -476,7 +476,9 @@
             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
@@ -578,7 +580,7 @@
           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