src/Pure/logic.ML

   val strip_imp_concl	: term -> term
   val strip_imp_prems	: term -> term list
   val strip_params	: term -> (string * typ) list
   val strip_prems	: int * term list * term -> term list * term
   val thaw_vars		: term -> term
-  val unvarifyT		: typ -> typ  
   val unvarify		: term -> term  
   val varify		: term -> term  
   end;
 
 functor LogicFun (structure Unify: UNIFY and Net:NET): LOGIC =

   | varify (Var(ixn,T)) = Var(ixn, Type.varifyT T)
   | varify (Abs (a,T,body)) = Abs (a, Type.varifyT T, varify body)
   | varify (f$t) = varify f $ varify t
   | varify t = t;
 
-(*Inverse of varifyT.  Move to Pure/type.ML?*)
-fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
-  | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
-  | unvarifyT T = T;
-
 (*Inverse of varify.  Converts axioms back to their original form.*)
-fun unvarify (Const(a,T))    = Const(a, unvarifyT T)
-  | unvarify (Var((a,0), T)) = Free(a, unvarifyT T)
-  | unvarify (Var(ixn,T))    = Var(ixn, unvarifyT T)	(*non-zero index!*)
-  | unvarify (Abs (a,T,body)) = Abs (a, unvarifyT T, unvarify body)
+fun unvarify (Const(a,T))    = Const(a, Type.unvarifyT T)
+  | unvarify (Var((a,0), T)) = Free(a, Type.unvarifyT T)
+  | unvarify (Var(ixn,T))    = Var(ixn, Type.unvarifyT T)  (*non-0 index!*)
+  | unvarify (Abs (a,T,body)) = Abs (a, Type.unvarifyT T, unvarify body)
   | unvarify (f$t) = unvarify f $ unvarify t
   | unvarify t = t;
 
 end;