# HG changeset patch
# User wenzelm
# Date 1131550001 -3600
# Node ID 9f03d8a9a81bc5ab8707a51b82c4ef24494f44da
# Parent  b74145e46e0d0d1bc75fc3da8b3598529eac9a79
Thm.varifyT': natural argument order;

diff -r b74145e46e0d -r 9f03d8a9a81b src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Wed Nov 09 12:21:05 2005 +0100
+++ b/src/HOL/Import/shuffler.ML	Wed Nov 09 16:26:41 2005 +0100
@@ -269,7 +269,7 @@
     let
 	val cU = ctyp_of sg U
 	val tfrees = add_term_tfrees (prop_of thm,[])
-	val (thm',rens) = varifyT'
+	val (rens, thm') = varifyT'
     (gen_rem (op = o apfst fst) (tfrees, name)) thm
 	val mid = 
 	    case rens of
diff -r b74145e46e0d -r 9f03d8a9a81b src/Pure/IsaPlanner/isand.ML
--- a/src/Pure/IsaPlanner/isand.ML	Wed Nov 09 12:21:05 2005 +0100
+++ b/src/Pure/IsaPlanner/isand.ML	Wed Nov 09 16:26:41 2005 +0100
@@ -224,7 +224,7 @@
     let 
       val varfiytfrees = (map (fn x => Term.dest_TFree (Thm.typ_of x)) ns)
       val skiptfrees = Term.add_term_tfrees (Thm.prop_of th,[]) \\ varfiytfrees;
-    in fst (Thm.varifyT' skiptfrees th) end;
+    in #2 (Thm.varifyT' skiptfrees th) end;
 
 (* change schematic/meta vars to fresh free vars *)
 fun fix_vars_to_frees_in_terms names ts = 
diff -r b74145e46e0d -r 9f03d8a9a81b src/Pure/IsaPlanner/rw_inst.ML
--- a/src/Pure/IsaPlanner/rw_inst.ML	Wed Nov 09 12:21:05 2005 +0100
+++ b/src/Pure/IsaPlanner/rw_inst.ML	Wed Nov 09 16:26:41 2005 +0100
@@ -296,8 +296,8 @@
         |> Drule.implies_intr_list cprems
         |> Drule.forall_intr_list frees_of_fixed_vars
         |> Drule.forall_elim_list vars
-        |> fst o Thm.varifyT' othertfrees
-        |> Drule.zero_var_indexes
+        |> Thm.varifyT' othertfrees
+        |-> K Drule.zero_var_indexes
     end;
 
 
diff -r b74145e46e0d -r 9f03d8a9a81b src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Wed Nov 09 12:21:05 2005 +0100
+++ b/src/Pure/Proof/proofchecker.ML	Wed Nov 09 16:26:41 2005 +0100
@@ -38,7 +38,7 @@
     fun thm_of_atom thm Ts =
       let
         val tvars = term_tvars (Thm.full_prop_of thm);
-        val (thm', fmap) = Thm.varifyT' [] thm;
+        val (fmap, thm') = Thm.varifyT' [] thm;
         val ctye = map (pairself (Thm.ctyp_of sg))
           (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
       in
diff -r b74145e46e0d -r 9f03d8a9a81b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Nov 09 12:21:05 2005 +0100
+++ b/src/Pure/thm.ML	Wed Nov 09 16:26:41 2005 +0100
@@ -114,7 +114,7 @@
   val trivial: cterm -> thm
   val class_triv: theory -> class -> thm
   val varifyT: thm -> thm
-  val varifyT': (string * sort) list -> thm -> thm * ((string * sort) * indexname) list
+  val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   val freezeT: thm -> thm
   val dest_state: thm * int -> (term * term) list * term list * term * term
   val lift_rule: cterm -> thm -> thm
@@ -1074,16 +1074,16 @@
     val (prop2, al) = Type.varify (prop1, tfrees);
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   in
-    (Thm {thy_ref = thy_ref,
+    (al, Thm {thy_ref = thy_ref,
       der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der,
       maxidx = Int.max (0, maxidx),
       shyps = shyps,
       hyps = hyps,
       tpairs = rev (map Logic.dest_equals ts),
-      prop = prop3}, al)
+      prop = prop3})
   end;
 
-val varifyT = #1 o varifyT' [];
+val varifyT = #2 o varifyT' [];
 
 (* Replace all TVars by new TFrees *)
 fun freezeT (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =