--- 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
--- 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 =
--- 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;
--- 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
--- 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}) =