# HG changeset patch
# User krauss
# Date 1269955530 -7200
# Node ID 85efdadee8aed0de5122baae687bafb2afe9a2d8
# Parent  8b25e3b217bce5f235def59a1e96e301b765ba97
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)

diff -r 8b25e3b217bc -r 85efdadee8ae src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Tue Mar 30 12:47:39 2010 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Tue Mar 30 15:25:30 2010 +0200
@@ -33,8 +33,8 @@
  \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
 
    "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %%  \
- \    (combination % TYPE('U) % TYPE('T) % f % g % x % y %% prf1 %% prf2)) ==  \
- \  (cong % TYPE('U) % TYPE('T) % f % g % x % y %%  \
+ \    (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) ==  \
+ \  (cong % TYPE('T) % TYPE('U) % f % g % x % y %%  \
  \    (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %%  \
  \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))",
 
@@ -52,20 +52,20 @@
  \  (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))",
 
    "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %%  \
- \    (abstract_rule % TYPE('U) % TYPE('T) % f % g %% prf)) ==  \
- \  (ext % TYPE('U) % TYPE('T) % f % g %%  \
+ \    (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) ==  \
+ \  (ext % TYPE('T) % TYPE('U) % f % g %%  \
  \    (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))",
 
    "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
  \    (eq_reflection % TYPE('T) % x % y %% prf)) == prf",
 
    "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
- \    (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %%  \
- \      (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %%  \
+ \    (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%  \
+ \      (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%  \
  \        (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) ==  \
  \  (iffD1 % A = C % B = D %%  \
- \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
- \      (cong % TYPE('T=>bool) % TYPE('T) %  \
+ \    (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %%  \
+ \      (cong % TYPE('T) % TYPE('T=>bool) %  \
  \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
  \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
  \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
@@ -74,12 +74,12 @@
 
    "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
  \    (axm.symmetric % TYPE('T2) % x5 % x6 %%  \
- \      (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %%  \
- \        (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %%  \
+ \      (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%  \
+ \        (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%  \
  \          (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) ==  \
  \  (iffD2 % A = C % B = D %%  \
- \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
- \      (cong % TYPE('T=>bool) % TYPE('T) %  \
+ \    (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %%  \
+ \      (cong % TYPE('T) % TYPE('T=>bool) %  \
  \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
  \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
  \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
@@ -91,14 +91,14 @@
    (* All *)
 
    "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
- \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
+ \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
  \  (allI % TYPE('a) % Q %%  \
  \    (Lam x.  \
  \        iffD1 % P x % Q x %% (prf % x) %%  \
  \         (spec % TYPE('a) % P % x %% prf')))",
 
    "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
- \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
+ \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
  \  (allI % TYPE('a) % P %%  \
  \    (Lam x.  \
  \        iffD2 % P x % Q x %% (prf % x) %%  \
@@ -107,14 +107,14 @@
    (* Ex *)
 
    "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
- \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
+ \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
  \  (exE % TYPE('a) % P % EX x. Q x %% prf' %%  \
  \    (Lam x H : P x.  \
  \        exI % TYPE('a) % Q % x %%  \
  \         (iffD1 % P x % Q x %% (prf % x) %% H)))",
 
    "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
- \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
+ \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
  \  (exE % TYPE('a) % Q % EX x. P x %% prf' %%  \
  \    (Lam x H : Q x.  \
  \        exI % TYPE('a) % P % x %%  \
@@ -139,7 +139,7 @@
    "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
  \    (HOL.refl % TYPE(bool=>bool) % op & A)) ==  \
  \  (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
- \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
+ \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
  \      (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %%  \
  \        (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %%  \
  \        (HOL.refl % TYPE(bool) % A)))",
@@ -163,7 +163,7 @@
    "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
  \    (HOL.refl % TYPE(bool=>bool) % op | A)) ==  \
  \  (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
- \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
+ \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
  \      (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %%  \
  \        (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %%  \
  \        (HOL.refl % TYPE(bool) % A)))",
@@ -185,7 +185,7 @@
    "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
  \    (HOL.refl % TYPE(bool=>bool) % op --> A)) ==  \
  \  (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
- \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
+ \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
  \      (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %%  \
  \        (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %%  \
  \        (HOL.refl % TYPE(bool) % A)))",
@@ -205,29 +205,29 @@
    (* = *)
 
    "(iffD1 % B % D %%  \
- \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
- \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
+ \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
+ \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
  \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
  \  (iffD1 % C % D %% prf2 %%  \
  \    (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
 
    "(iffD2 % B % D %%  \
- \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
- \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
+ \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
+ \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
  \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
  \  (iffD1 % A % B %% prf1 %%  \
  \    (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
 
    "(iffD1 % A % C %%  \
- \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
- \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
+ \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
+ \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
  \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)==  \
  \  (iffD2 % C % D %% prf2 %%  \
  \    (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
 
    "(iffD2 % A % C %%  \
- \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
- \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
+ \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
+ \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
  \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
  \  (iffD2 % A % B %% prf1 %%  \
  \    (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
@@ -235,7 +235,7 @@
    "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
  \    (HOL.refl % TYPE(bool=>bool) % op = A)) ==  \
  \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
- \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
+ \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
  \      (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%  \
  \        (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
  \        (HOL.refl % TYPE(bool) % A)))",
diff -r 8b25e3b217bc -r 85efdadee8ae src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Mar 30 12:47:39 2010 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Mar 30 15:25:30 2010 +0200
@@ -541,7 +541,7 @@
           let
             val prf = join_proof body;
             val (vs', tye) = find_inst prop Ts ts vs;
-            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye;
+            val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye;
             val T = etype_of thy' vs' [] prop;
             val defs' = if T = nullT then defs
               else fst (extr d defs vs ts Ts hs prf0)
@@ -562,7 +562,7 @@
                     val corr_prf' = List.foldr forall_intr_prf
                       (proof_combt
                          (PThm (serial (),
-                          ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
+                          ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
                             Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
                       (map (get_var_type corr_prop) (vfs_of prop))
                   in
@@ -580,7 +580,7 @@
       | corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
           let
             val (vs', tye) = find_inst prop Ts ts vs;
-            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
+            val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
           in
             if etype_of thy' vs' [] prop = nullT andalso
               realizes_null vs' prop aconv prop then (defs, prf0)
@@ -631,7 +631,7 @@
           let
             val prf = join_proof body;
             val (vs', tye) = find_inst prop Ts ts vs;
-            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
+            val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
           in
             case Symtab.lookup realizers s of
               NONE => (case find vs' (find' s defs) of
@@ -665,15 +665,15 @@
                     val corr_prf' =
                       chtype [] equal_elim_axm %> lhs %> rhs %%
                        (chtype [propT] symmetric_axm %> rhs %> lhs %%
-                         (chtype [propT, T] combination_axm %> f %> f %> c %> t' %%
+                         (chtype [T, propT] combination_axm %> f %> f %> c %> t' %%
                            (chtype [T --> propT] reflexive_axm %> f) %%
                            PAxm (cname ^ "_def", eqn,
-                             SOME (map TVar (OldTerm.term_tvars eqn))))) %% corr_prf;
+                             SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf;
                     val corr_prop = Reconstruct.prop_of corr_prf';
                     val corr_prf'' = List.foldr forall_intr_prf
                       (proof_combt
                         (PThm (serial (),
-                         ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
+                         ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
                            Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
                       (map (get_var_type corr_prop) (vfs_of prop));
                   in
@@ -691,7 +691,7 @@
       | extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) =
           let
             val (vs', tye) = find_inst prop Ts ts vs;
-            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
+            val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
           in
             case find vs' (Symtab.lookup_list realizers s) of
               SOME (t, _) => (defs, subst_TVars tye' t)
diff -r 8b25e3b217bc -r 85efdadee8ae src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Mar 30 12:47:39 2010 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Mar 30 15:25:30 2010 +0200
@@ -179,7 +179,7 @@
           (PAxm ("Pure.reflexive", _, _) % _)) =
         let val (U, V) = (case T of
           Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
-        in SOME (prf %% (ax combination_axm [V, U] %> eq % ?? eq % ?? t % ?? t %%
+        in SOME (prf %% (ax combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %%
           (ax reflexive_axm [T] % ?? eq) %% (ax reflexive_axm [U] % ?? t)))
         end
 
@@ -229,7 +229,7 @@
           if member (op =) defs s then
             let
               val vs = vars_of prop;
-              val tvars = OldTerm.term_tvars prop;
+              val tvars = Term.add_tvars prop [] |> rev;
               val (_, rhs) = Logic.dest_equals prop;
               val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
                 (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
diff -r 8b25e3b217bc -r 85efdadee8ae src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Tue Mar 30 12:47:39 2010 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Tue Mar 30 15:25:30 2010 +0200
@@ -35,7 +35,7 @@
 
     fun thm_of_atom thm Ts =
       let
-        val tvars = OldTerm.term_tvars (Thm.full_prop_of thm);
+        val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
         val (fmap, thm') = Thm.varifyT_global' [] thm;
         val ctye = map (pairself (Thm.ctyp_of thy))
           (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
diff -r 8b25e3b217bc -r 85efdadee8ae src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Tue Mar 30 12:47:39 2010 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Tue Mar 30 15:25:30 2010 +0200
@@ -136,8 +136,8 @@
 
     fun mk_cnstrts_atom env vTs prop opTs prf =
           let
-            val tvars = OldTerm.term_tvars prop;
-            val tfrees = OldTerm.term_tfrees prop;
+            val tvars = Term.add_tvars prop [] |> rev;
+            val tfrees = Term.add_tfrees prop [] |> rev;
             val (Ts, env') =
               (case opTs of
                 NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
@@ -304,7 +304,7 @@
   end;
 
 fun prop_of_atom prop Ts = subst_atomic_types
-  (map TVar (OldTerm.term_tvars prop) @ map TFree (OldTerm.term_tfrees prop) ~~ Ts)
+  (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts)
   (forall_intr_vfs prop);
 
 val head_norm = Envir.head_norm (Envir.empty 0);
@@ -370,9 +370,9 @@
                   end
               | SOME (maxidx', prf) => (maxidx' + maxidx + 1,
                   incr_indexes (maxidx + 1) prf, prfs));
-            val tfrees = OldTerm.term_tfrees prop;
+            val tfrees = Term.add_tfrees prop [] |> rev;
             val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j))
-              (OldTerm.term_tvars prop) @ map (rpair ~1 o fst) tfrees ~~ Ts;
+              (Term.add_tvars prop [] |> rev) @ map (rpair ~1 o fst) tfrees ~~ Ts;
             val varify = map_type_tfree (fn p as (a, S) =>
               if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
           in