--- 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;
--- 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;