switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
authorkrauss
Tue Mar 30 15:25:30 2010 +0200 (2010-03-30)
changeset 3604285efdadee8ae
parent 36041 8b25e3b217bc
child 36043 d149c3886e7e
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
src/HOL/Tools/rewrite_hol_proof.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Proof/proofchecker.ML
src/Pure/Proof/reconstruct.ML
     1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Tue Mar 30 12:47:39 2010 +0200
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Tue Mar 30 15:25:30 2010 +0200
     1.3 @@ -33,8 +33,8 @@
     1.4   \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
     1.5  
     1.6     "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %%  \
     1.7 - \    (combination % TYPE('U) % TYPE('T) % f % g % x % y %% prf1 %% prf2)) ==  \
     1.8 - \  (cong % TYPE('U) % TYPE('T) % f % g % x % y %%  \
     1.9 + \    (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) ==  \
    1.10 + \  (cong % TYPE('T) % TYPE('U) % f % g % x % y %%  \
    1.11   \    (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %%  \
    1.12   \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))",
    1.13  
    1.14 @@ -52,20 +52,20 @@
    1.15   \  (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))",
    1.16  
    1.17     "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %%  \
    1.18 - \    (abstract_rule % TYPE('U) % TYPE('T) % f % g %% prf)) ==  \
    1.19 - \  (ext % TYPE('U) % TYPE('T) % f % g %%  \
    1.20 + \    (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) ==  \
    1.21 + \  (ext % TYPE('T) % TYPE('U) % f % g %%  \
    1.22   \    (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))",
    1.23  
    1.24     "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
    1.25   \    (eq_reflection % TYPE('T) % x % y %% prf)) == prf",
    1.26  
    1.27     "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
    1.28 - \    (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %%  \
    1.29 - \      (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %%  \
    1.30 + \    (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%  \
    1.31 + \      (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%  \
    1.32   \        (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) ==  \
    1.33   \  (iffD1 % A = C % B = D %%  \
    1.34 - \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
    1.35 - \      (cong % TYPE('T=>bool) % TYPE('T) %  \
    1.36 + \    (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %%  \
    1.37 + \      (cong % TYPE('T) % TYPE('T=>bool) %  \
    1.38   \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
    1.39   \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
    1.40   \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
    1.41 @@ -74,12 +74,12 @@
    1.42  
    1.43     "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
    1.44   \    (axm.symmetric % TYPE('T2) % x5 % x6 %%  \
    1.45 - \      (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %%  \
    1.46 - \        (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %%  \
    1.47 + \      (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%  \
    1.48 + \        (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%  \
    1.49   \          (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) ==  \
    1.50   \  (iffD2 % A = C % B = D %%  \
    1.51 - \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
    1.52 - \      (cong % TYPE('T=>bool) % TYPE('T) %  \
    1.53 + \    (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %%  \
    1.54 + \      (cong % TYPE('T) % TYPE('T=>bool) %  \
    1.55   \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
    1.56   \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
    1.57   \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
    1.58 @@ -91,14 +91,14 @@
    1.59     (* All *)
    1.60  
    1.61     "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
    1.62 - \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
    1.63 + \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
    1.64   \  (allI % TYPE('a) % Q %%  \
    1.65   \    (Lam x.  \
    1.66   \        iffD1 % P x % Q x %% (prf % x) %%  \
    1.67   \         (spec % TYPE('a) % P % x %% prf')))",
    1.68  
    1.69     "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
    1.70 - \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
    1.71 + \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
    1.72   \  (allI % TYPE('a) % P %%  \
    1.73   \    (Lam x.  \
    1.74   \        iffD2 % P x % Q x %% (prf % x) %%  \
    1.75 @@ -107,14 +107,14 @@
    1.76     (* Ex *)
    1.77  
    1.78     "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
    1.79 - \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
    1.80 + \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
    1.81   \  (exE % TYPE('a) % P % EX x. Q x %% prf' %%  \
    1.82   \    (Lam x H : P x.  \
    1.83   \        exI % TYPE('a) % Q % x %%  \
    1.84   \         (iffD1 % P x % Q x %% (prf % x) %% H)))",
    1.85  
    1.86     "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
    1.87 - \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
    1.88 + \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
    1.89   \  (exE % TYPE('a) % Q % EX x. P x %% prf' %%  \
    1.90   \    (Lam x H : Q x.  \
    1.91   \        exI % TYPE('a) % P % x %%  \
    1.92 @@ -139,7 +139,7 @@
    1.93     "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
    1.94   \    (HOL.refl % TYPE(bool=>bool) % op & A)) ==  \
    1.95   \  (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
    1.96 - \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
    1.97 + \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
    1.98   \      (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %%  \
    1.99   \        (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %%  \
   1.100   \        (HOL.refl % TYPE(bool) % A)))",
   1.101 @@ -163,7 +163,7 @@
   1.102     "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
   1.103   \    (HOL.refl % TYPE(bool=>bool) % op | A)) ==  \
   1.104   \  (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
   1.105 - \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
   1.106 + \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   1.107   \      (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %%  \
   1.108   \        (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %%  \
   1.109   \        (HOL.refl % TYPE(bool) % A)))",
   1.110 @@ -185,7 +185,7 @@
   1.111     "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
   1.112   \    (HOL.refl % TYPE(bool=>bool) % op --> A)) ==  \
   1.113   \  (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
   1.114 - \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
   1.115 + \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   1.116   \      (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %%  \
   1.117   \        (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %%  \
   1.118   \        (HOL.refl % TYPE(bool) % A)))",
   1.119 @@ -205,29 +205,29 @@
   1.120     (* = *)
   1.121  
   1.122     "(iffD1 % B % D %%  \
   1.123 - \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
   1.124 - \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
   1.125 + \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
   1.126 + \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
   1.127   \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.128   \  (iffD1 % C % D %% prf2 %%  \
   1.129   \    (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
   1.130  
   1.131     "(iffD2 % B % D %%  \
   1.132 - \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
   1.133 - \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
   1.134 + \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
   1.135 + \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
   1.136   \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.137   \  (iffD1 % A % B %% prf1 %%  \
   1.138   \    (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
   1.139  
   1.140     "(iffD1 % A % C %%  \
   1.141 - \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
   1.142 - \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
   1.143 + \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
   1.144 + \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
   1.145   \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)==  \
   1.146   \  (iffD2 % C % D %% prf2 %%  \
   1.147   \    (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
   1.148  
   1.149     "(iffD2 % A % C %%  \
   1.150 - \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
   1.151 - \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
   1.152 + \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
   1.153 + \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
   1.154   \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.155   \  (iffD2 % A % B %% prf1 %%  \
   1.156   \    (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
   1.157 @@ -235,7 +235,7 @@
   1.158     "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
   1.159   \    (HOL.refl % TYPE(bool=>bool) % op = A)) ==  \
   1.160   \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
   1.161 - \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
   1.162 + \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   1.163   \      (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%  \
   1.164   \        (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
   1.165   \        (HOL.refl % TYPE(bool) % A)))",
     2.1 --- a/src/Pure/Proof/extraction.ML	Tue Mar 30 12:47:39 2010 +0200
     2.2 +++ b/src/Pure/Proof/extraction.ML	Tue Mar 30 15:25:30 2010 +0200
     2.3 @@ -541,7 +541,7 @@
     2.4            let
     2.5              val prf = join_proof body;
     2.6              val (vs', tye) = find_inst prop Ts ts vs;
     2.7 -            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye;
     2.8 +            val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye;
     2.9              val T = etype_of thy' vs' [] prop;
    2.10              val defs' = if T = nullT then defs
    2.11                else fst (extr d defs vs ts Ts hs prf0)
    2.12 @@ -562,7 +562,7 @@
    2.13                      val corr_prf' = List.foldr forall_intr_prf
    2.14                        (proof_combt
    2.15                           (PThm (serial (),
    2.16 -                          ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
    2.17 +                          ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
    2.18                              Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
    2.19                        (map (get_var_type corr_prop) (vfs_of prop))
    2.20                    in
    2.21 @@ -580,7 +580,7 @@
    2.22        | corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
    2.23            let
    2.24              val (vs', tye) = find_inst prop Ts ts vs;
    2.25 -            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
    2.26 +            val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
    2.27            in
    2.28              if etype_of thy' vs' [] prop = nullT andalso
    2.29                realizes_null vs' prop aconv prop then (defs, prf0)
    2.30 @@ -631,7 +631,7 @@
    2.31            let
    2.32              val prf = join_proof body;
    2.33              val (vs', tye) = find_inst prop Ts ts vs;
    2.34 -            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
    2.35 +            val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
    2.36            in
    2.37              case Symtab.lookup realizers s of
    2.38                NONE => (case find vs' (find' s defs) of
    2.39 @@ -665,15 +665,15 @@
    2.40                      val corr_prf' =
    2.41                        chtype [] equal_elim_axm %> lhs %> rhs %%
    2.42                         (chtype [propT] symmetric_axm %> rhs %> lhs %%
    2.43 -                         (chtype [propT, T] combination_axm %> f %> f %> c %> t' %%
    2.44 +                         (chtype [T, propT] combination_axm %> f %> f %> c %> t' %%
    2.45                             (chtype [T --> propT] reflexive_axm %> f) %%
    2.46                             PAxm (cname ^ "_def", eqn,
    2.47 -                             SOME (map TVar (OldTerm.term_tvars eqn))))) %% corr_prf;
    2.48 +                             SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf;
    2.49                      val corr_prop = Reconstruct.prop_of corr_prf';
    2.50                      val corr_prf'' = List.foldr forall_intr_prf
    2.51                        (proof_combt
    2.52                          (PThm (serial (),
    2.53 -                         ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
    2.54 +                         ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
    2.55                             Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
    2.56                        (map (get_var_type corr_prop) (vfs_of prop));
    2.57                    in
    2.58 @@ -691,7 +691,7 @@
    2.59        | extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) =
    2.60            let
    2.61              val (vs', tye) = find_inst prop Ts ts vs;
    2.62 -            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
    2.63 +            val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
    2.64            in
    2.65              case find vs' (Symtab.lookup_list realizers s) of
    2.66                SOME (t, _) => (defs, subst_TVars tye' t)
     3.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Mar 30 12:47:39 2010 +0200
     3.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Mar 30 15:25:30 2010 +0200
     3.3 @@ -179,7 +179,7 @@
     3.4            (PAxm ("Pure.reflexive", _, _) % _)) =
     3.5          let val (U, V) = (case T of
     3.6            Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
     3.7 -        in SOME (prf %% (ax combination_axm [V, U] %> eq % ?? eq % ?? t % ?? t %%
     3.8 +        in SOME (prf %% (ax combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %%
     3.9            (ax reflexive_axm [T] % ?? eq) %% (ax reflexive_axm [U] % ?? t)))
    3.10          end
    3.11  
    3.12 @@ -229,7 +229,7 @@
    3.13            if member (op =) defs s then
    3.14              let
    3.15                val vs = vars_of prop;
    3.16 -              val tvars = OldTerm.term_tvars prop;
    3.17 +              val tvars = Term.add_tvars prop [] |> rev;
    3.18                val (_, rhs) = Logic.dest_equals prop;
    3.19                val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
    3.20                  (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
     4.1 --- a/src/Pure/Proof/proofchecker.ML	Tue Mar 30 12:47:39 2010 +0200
     4.2 +++ b/src/Pure/Proof/proofchecker.ML	Tue Mar 30 15:25:30 2010 +0200
     4.3 @@ -35,7 +35,7 @@
     4.4  
     4.5      fun thm_of_atom thm Ts =
     4.6        let
     4.7 -        val tvars = OldTerm.term_tvars (Thm.full_prop_of thm);
     4.8 +        val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
     4.9          val (fmap, thm') = Thm.varifyT_global' [] thm;
    4.10          val ctye = map (pairself (Thm.ctyp_of thy))
    4.11            (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
     5.1 --- a/src/Pure/Proof/reconstruct.ML	Tue Mar 30 12:47:39 2010 +0200
     5.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Mar 30 15:25:30 2010 +0200
     5.3 @@ -136,8 +136,8 @@
     5.4  
     5.5      fun mk_cnstrts_atom env vTs prop opTs prf =
     5.6            let
     5.7 -            val tvars = OldTerm.term_tvars prop;
     5.8 -            val tfrees = OldTerm.term_tfrees prop;
     5.9 +            val tvars = Term.add_tvars prop [] |> rev;
    5.10 +            val tfrees = Term.add_tfrees prop [] |> rev;
    5.11              val (Ts, env') =
    5.12                (case opTs of
    5.13                  NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
    5.14 @@ -304,7 +304,7 @@
    5.15    end;
    5.16  
    5.17  fun prop_of_atom prop Ts = subst_atomic_types
    5.18 -  (map TVar (OldTerm.term_tvars prop) @ map TFree (OldTerm.term_tfrees prop) ~~ Ts)
    5.19 +  (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts)
    5.20    (forall_intr_vfs prop);
    5.21  
    5.22  val head_norm = Envir.head_norm (Envir.empty 0);
    5.23 @@ -370,9 +370,9 @@
    5.24                    end
    5.25                | SOME (maxidx', prf) => (maxidx' + maxidx + 1,
    5.26                    incr_indexes (maxidx + 1) prf, prfs));
    5.27 -            val tfrees = OldTerm.term_tfrees prop;
    5.28 +            val tfrees = Term.add_tfrees prop [] |> rev;
    5.29              val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j))
    5.30 -              (OldTerm.term_tvars prop) @ map (rpair ~1 o fst) tfrees ~~ Ts;
    5.31 +              (Term.add_tvars prop [] |> rev) @ map (rpair ~1 o fst) tfrees ~~ Ts;
    5.32              val varify = map_type_tfree (fn p as (a, S) =>
    5.33                if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
    5.34            in