--- a/src/Pure/logic.ML Thu Jun 05 13:29:41 1997 +0200
+++ b/src/Pure/logic.ML Thu Jun 05 13:30:24 1997 +0200
@@ -20,7 +20,6 @@
val dest_inclass : term -> typ * class
val dest_type : term -> typ
val flatten_params : int -> term -> term
- val freeze_vars : term -> term
val incr_indexes : typ list * int -> term -> term
val lift_fns : term * int -> (term -> term) * (term -> term)
val list_flexpairs : (term*term)list * term -> term
@@ -44,7 +43,6 @@
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 unvarify : term -> term
val varify : term -> term
val termord : term * term -> order
@@ -174,29 +172,6 @@
A);
-(*Freeze all (T)Vars by turning them into (T)Frees*)
-fun freeze_vars(Var(ixn,T)) = Free(Syntax.string_of_vname ixn,
- Type.freeze_vars T)
- | freeze_vars(Const(a,T)) = Const(a,Type.freeze_vars T)
- | freeze_vars(Free(a,T)) = Free(a,Type.freeze_vars T)
- | freeze_vars(s$t) = freeze_vars s $ freeze_vars t
- | freeze_vars(Abs(a,T,t)) = Abs(a,Type.freeze_vars T,freeze_vars t)
- | freeze_vars(b) = b;
-
-(*Reverse the effect of freeze_vars*)
-fun thaw_vars(Const(a,T)) = Const(a,Type.thaw_vars T)
- | thaw_vars(Free(a,T)) =
- let val T' = Type.thaw_vars T
- in case explode a of
- "?"::vn => let val (ixn,_) = Syntax.scan_varname vn
- in Var(ixn,T') end
- | _ => Free(a,T')
- end
- | thaw_vars(Abs(a,T,t)) = Abs(a,Type.thaw_vars T, thaw_vars t)
- | thaw_vars(s$t) = thaw_vars s $ thaw_vars t
- | thaw_vars(b) = b;
-
-
(*** Specialized operations for resolution... ***)
(*For all variables in the term, increment indexnames and lift over the Us