src/Pure/Proof/extraction.ML
changeset 36042 85efdadee8ae
parent 35985 0bbf0d2348f9
child 36620 e6bb250402b5
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Mar 30 12:47:39 2010 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Mar 30 15:25:30 2010 +0200
     1.3 @@ -541,7 +541,7 @@
     1.4            let
     1.5              val prf = join_proof body;
     1.6              val (vs', tye) = find_inst prop Ts ts vs;
     1.7 -            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye;
     1.8 +            val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ 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 @@ -562,7 +562,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 (OldTerm.term_tvars corr_prop))),
    1.17 +                          ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
    1.18                              Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
    1.19                        (map (get_var_type corr_prop) (vfs_of prop))
    1.20                    in
    1.21 @@ -580,7 +580,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 (OldTerm.term_tvars prop) ~~ Ts') @ tye
    1.26 +            val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ 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 @@ -631,7 +631,7 @@
    1.31            let
    1.32              val prf = join_proof body;
    1.33              val (vs', tye) = find_inst prop Ts ts vs;
    1.34 -            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
    1.35 +            val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ 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 @@ -665,15 +665,15 @@
    1.40                      val corr_prf' =
    1.41                        chtype [] equal_elim_axm %> lhs %> rhs %%
    1.42                         (chtype [propT] symmetric_axm %> rhs %> lhs %%
    1.43 -                         (chtype [propT, T] combination_axm %> f %> f %> c %> t' %%
    1.44 +                         (chtype [T, propT] combination_axm %> f %> f %> c %> t' %%
    1.45                             (chtype [T --> propT] reflexive_axm %> f) %%
    1.46                             PAxm (cname ^ "_def", eqn,
    1.47 -                             SOME (map TVar (OldTerm.term_tvars eqn))))) %% corr_prf;
    1.48 +                             SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf;
    1.49                      val corr_prop = Reconstruct.prop_of corr_prf';
    1.50                      val corr_prf'' = List.foldr forall_intr_prf
    1.51                        (proof_combt
    1.52                          (PThm (serial (),
    1.53 -                         ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
    1.54 +                         ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
    1.55                             Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
    1.56                        (map (get_var_type corr_prop) (vfs_of prop));
    1.57                    in
    1.58 @@ -691,7 +691,7 @@
    1.59        | extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) =
    1.60            let
    1.61              val (vs', tye) = find_inst prop Ts ts vs;
    1.62 -            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
    1.63 +            val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
    1.64            in
    1.65              case find vs' (Symtab.lookup_list realizers s) of
    1.66                SOME (t, _) => (defs, subst_TVars tye' t)