# HG changeset patch
# User wenzelm
# Date 928607429 -7200
# Node ID 0af1797d5315c0ca2b8cc04b2d5225a9feff2eb3
# Parent  10b77354862bf03fe30b32a5cd85c6e5448ac099
varifyT': observe additional 'fixed' tfrees;

diff -r 10b77354862b -r 0af1797d5315 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Jun 05 20:29:07 1999 +0200
+++ b/src/Pure/thm.ML	Sat Jun 05 20:30:29 1999 +0200
@@ -72,7 +72,7 @@
     | Bicompose           of bool * bool * int * int * Envir.env
     | Flexflex_rule       of Envir.env            
     | Class_triv          of class       
-    | VarifyT
+    | VarifyT		  of string list
     | FreezeT
     | RewriteC            of cterm
     | CongC               of cterm
@@ -131,6 +131,7 @@
   val trivial           : cterm -> thm
   val class_triv        : Sign.sg -> class -> thm
   val varifyT           : thm -> thm
+  val varifyT'          : string list -> thm -> thm
   val freezeT           : thm -> thm
   val dest_state        : thm * int ->
     (term * term) list * term list * term * term
@@ -347,7 +348,7 @@
   | Flexflex_rule       of Envir.env            (*identifies unifier chosen*)
 (*other derived rules*)
   | Class_triv          of class
-  | VarifyT
+  | VarifyT		of string list
   | FreezeT
 (*for the simplifier*)
   | RewriteC            of cterm
@@ -1140,12 +1141,12 @@
   end;
 
 
-(* Replace all TFrees not in the hyps by new TVars *)
-fun varifyT(Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
-  let val tfrees = foldr add_term_tfree_names (hyps,[])
+(* Replace all TFrees not fixed or in the hyps by new TVars *)
+fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
+  let val tfrees = foldr add_term_tfree_names (hyps,fixed)
   in let val thm = (*no fix_shyps*)
     Thm{sign_ref = sign_ref, 
-        der = infer_derivs (VarifyT, [der]), 
+        der = infer_derivs (VarifyT fixed, [der]), 
         maxidx = Int.max(0,maxidx), 
         shyps = shyps, 
         hyps = hyps,
@@ -1155,6 +1156,8 @@
 duplicate TVars with differnt sorts *)
   end;
 
+val varifyT = varifyT' [];
+
 (* Replace all TVars by new TFrees *)
 fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
   let val (prop',_) = Type.freeze_thaw prop