src/Pure/Proof/extraction.ML
changeset 29270 0eade173f77e
parent 29265 5b4247055bd7
child 29579 cb520b766e00
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Dec 31 15:30:10 2008 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Dec 31 18:53:16 2008 +0100
     1.3 @@ -548,7 +548,7 @@
     1.4            let
     1.5              val prf = force_proof body;
     1.6              val (vs', tye) = find_inst prop Ts ts vs;
     1.7 -            val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye;
     1.8 +            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye;
     1.9              val T = etype_of thy' vs' [] prop;
    1.10              val defs' = if T = nullT then defs
    1.11                else fst (extr d defs vs ts Ts hs prf0)
    1.12 @@ -569,7 +569,7 @@
    1.13                      val corr_prf' = List.foldr forall_intr_prf
    1.14                        (proof_combt
    1.15                           (PThm (serial (),
    1.16 -                          ((corr_name name vs', corr_prop, SOME (map TVar (term_tvars corr_prop))),
    1.17 +                          ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
    1.18                              Lazy.value (make_proof_body corr_prf))), vfs_of corr_prop))
    1.19                        (map (get_var_type corr_prop) (vfs_of prop))
    1.20                    in
    1.21 @@ -587,7 +587,7 @@
    1.22        | corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
    1.23            let
    1.24              val (vs', tye) = find_inst prop Ts ts vs;
    1.25 -            val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
    1.26 +            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
    1.27            in
    1.28              if etype_of thy' vs' [] prop = nullT andalso
    1.29                realizes_null vs' prop aconv prop then (defs, prf0)
    1.30 @@ -638,7 +638,7 @@
    1.31            let
    1.32              val prf = force_proof body;
    1.33              val (vs', tye) = find_inst prop Ts ts vs;
    1.34 -            val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
    1.35 +            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
    1.36            in
    1.37              case Symtab.lookup realizers s of
    1.38                NONE => (case find vs' (find' s defs) of
    1.39 @@ -675,12 +675,12 @@
    1.40                           (chtype [propT, T] combination_axm %> f %> f %> c %> t' %%
    1.41                             (chtype [T --> propT] reflexive_axm %> f) %%
    1.42                             PAxm (cname ^ "_def", eqn,
    1.43 -                             SOME (map TVar (term_tvars eqn))))) %% corr_prf;
    1.44 +                             SOME (map TVar (OldTerm.term_tvars eqn))))) %% corr_prf;
    1.45                      val corr_prop = Reconstruct.prop_of corr_prf';
    1.46                      val corr_prf'' = List.foldr forall_intr_prf
    1.47                        (proof_combt
    1.48                          (PThm (serial (),
    1.49 -                         ((corr_name s vs', corr_prop, SOME (map TVar (term_tvars corr_prop))),
    1.50 +                         ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
    1.51                             Lazy.value (make_proof_body corr_prf'))), vfs_of corr_prop))
    1.52                        (map (get_var_type corr_prop) (vfs_of prop));
    1.53                    in
    1.54 @@ -698,7 +698,7 @@
    1.55        | extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) =
    1.56            let
    1.57              val (vs', tye) = find_inst prop Ts ts vs;
    1.58 -            val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
    1.59 +            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
    1.60            in
    1.61              case find vs' (Symtab.lookup_list realizers s) of
    1.62                SOME (t, _) => (defs, subst_TVars tye' t)