src/Pure/logic.ML
changeset 3408 98a2d517cabe
parent 2508 ce48daa388a7
child 3893 5a1f22e7b359
     1.1 --- a/src/Pure/logic.ML	Thu Jun 05 13:29:41 1997 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu Jun 05 13:30:24 1997 +0200
     1.3 @@ -20,7 +20,6 @@
     1.4    val dest_inclass	: term -> typ * class
     1.5    val dest_type		: term -> typ
     1.6    val flatten_params	: int -> term -> term
     1.7 -  val freeze_vars	: term -> term
     1.8    val incr_indexes	: typ list * int -> term -> term
     1.9    val lift_fns		: term * int -> (term -> term) * (term -> term)
    1.10    val list_flexpairs	: (term*term)list * term -> term
    1.11 @@ -44,7 +43,6 @@
    1.12    val strip_imp_prems	: term -> term list
    1.13    val strip_params	: term -> (string * typ) list
    1.14    val strip_prems	: int * term list * term -> term list * term
    1.15 -  val thaw_vars		: term -> term
    1.16    val unvarify		: term -> term
    1.17    val varify		: term -> term
    1.18    val termord		: term * term -> order
    1.19 @@ -174,29 +172,6 @@
    1.20  		   A);
    1.21  
    1.22  
    1.23 -(*Freeze all (T)Vars by turning them into (T)Frees*)
    1.24 -fun freeze_vars(Var(ixn,T)) = Free(Syntax.string_of_vname ixn,
    1.25 -                                   Type.freeze_vars T)
    1.26 -  | freeze_vars(Const(a,T)) = Const(a,Type.freeze_vars T)
    1.27 -  | freeze_vars(Free(a,T))  = Free(a,Type.freeze_vars T)
    1.28 -  | freeze_vars(s$t)        = freeze_vars s $ freeze_vars t
    1.29 -  | freeze_vars(Abs(a,T,t)) = Abs(a,Type.freeze_vars T,freeze_vars t)
    1.30 -  | freeze_vars(b)          = b;
    1.31 -
    1.32 -(*Reverse the effect of freeze_vars*)
    1.33 -fun thaw_vars(Const(a,T)) = Const(a,Type.thaw_vars T)
    1.34 -  | thaw_vars(Free(a,T))  =
    1.35 -      let val T' = Type.thaw_vars T
    1.36 -      in case explode a of
    1.37 -	   "?"::vn => let val (ixn,_) = Syntax.scan_varname vn
    1.38 -                      in Var(ixn,T') end
    1.39 -	 | _       => Free(a,T')
    1.40 -      end
    1.41 -  | thaw_vars(Abs(a,T,t)) = Abs(a,Type.thaw_vars T, thaw_vars t)
    1.42 -  | thaw_vars(s$t)        = thaw_vars s $ thaw_vars t
    1.43 -  | thaw_vars(b)          = b;
    1.44 -
    1.45 -
    1.46  (*** Specialized operations for resolution... ***)
    1.47  
    1.48  (*For all variables in the term, increment indexnames and lift over the Us