# HG changeset patch
# User lcp
# Date 778852013 -7200
# Node ID 409c9ee7a9f30fbfb9ad5cf127037c64468cb9ae
# Parent  5b1a0e50c79a6da05c6cf3a61d968d26511ad263
Pure/type/unvarifyT: moved there from logic.ML

diff -r 5b1a0e50c79a -r 409c9ee7a9f3 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Sep 06 13:28:56 1994 +0200
+++ b/src/Pure/logic.ML	Tue Sep 06 13:46:53 1994 +0200
@@ -44,7 +44,6 @@
   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;
@@ -320,16 +319,11 @@
   | 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;
 
diff -r 5b1a0e50c79a -r 409c9ee7a9f3 src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Sep 06 13:28:56 1994 +0200
+++ b/src/Pure/type.ML	Tue Sep 06 13:46:53 1994 +0200
@@ -53,6 +53,7 @@
   val unify: type_sig -> (typ * typ) * (indexname * typ) list
     -> (indexname * typ) list
   val raw_unify: typ * typ -> bool
+  val unvarifyT		: typ -> typ  
   val varifyT: typ -> typ
   val varify: term * string list -> term
   exception TUNIFY
@@ -1060,6 +1061,11 @@
   | varifyT (TFree (a, S)) = TVar ((a, 0), S)
   | varifyT T = T;
 
+(*Inverse of varifyT*)
+fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
+  | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
+  | unvarifyT T = T;
+
 (* Turn TFrees except those in fixed into new TVars *)
 fun varify (t, fixed) =
   let val fs = add_term_tfree_names(t, []) \\ fixed;