src/Pure/Proof/extraction.ML
changeset 13609 73c3915553b4
parent 13417 12cc77f90811
child 13714 bdd483321f4b
     1.1 --- a/src/Pure/Proof/extraction.ML	Mon Sep 30 16:40:57 2002 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon Sep 30 16:42:46 2002 +0200
     1.3 @@ -445,7 +445,7 @@
     1.4              val defs' = if T = nullT then defs
     1.5                else fst (extr d defs vs ts Ts hs prf0)
     1.6            in
     1.7 -            if T = nullT andalso realizes_null vs' prop = prop then (defs, prf0)
     1.8 +            if T = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0)
     1.9              else case Symtab.lookup (realizers, name) of
    1.10                None => (case find vs' (find' name defs') of
    1.11                  None =>
    1.12 @@ -476,7 +476,9 @@
    1.13              val (vs', tye) = find_inst prop Ts ts vs;
    1.14              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
    1.15            in
    1.16 -            case find vs' (Symtab.lookup_multi (realizers, s)) of
    1.17 +            if etype_of sg vs' [] prop = nullT andalso
    1.18 +              realizes_null vs' prop aconv prop then (defs, prf0)
    1.19 +            else case find vs' (Symtab.lookup_multi (realizers, s)) of
    1.20                Some (_, prf) => (defs, prf_subst_TVars tye' prf)
    1.21              | None => error ("corr: no realizer for instance of axiom " ^
    1.22                  quote s ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
    1.23 @@ -578,7 +580,7 @@
    1.24            in
    1.25              case find vs' (Symtab.lookup_multi (realizers, s)) of
    1.26                Some (t, _) => (defs, subst_TVars tye' t)
    1.27 -            | None => error ("no realizer for instance of axiom " ^
    1.28 +            | None => error ("extr: no realizer for instance of axiom " ^
    1.29                  quote s ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
    1.30                    (Reconstruct.prop_of (proof_combt (prf0, ts)))))
    1.31            end