src/Pure/logic.ML
changeset 32004 6ef7056e5215
parent 31981 9c59cbb9c5a2
child 32008 fa0cc3c8f73d
     1.1 --- a/src/Pure/logic.ML	Tue Jul 14 12:10:44 2009 +0200
     1.2 +++ b/src/Pure/logic.ML	Tue Jul 14 12:18:52 2009 +0200
     1.3 @@ -71,9 +71,7 @@
     1.4    val varify: term -> term
     1.5    val unvarify: term -> term
     1.6    val legacy_varifyT: typ -> typ
     1.7 -  val legacy_unvarifyT: typ -> typ
     1.8    val legacy_varify: term -> term
     1.9 -  val legacy_unvarify: term -> term
    1.10    val get_goal: term -> int -> term
    1.11    val goal_params: term -> int -> term * term list
    1.12    val prems_of_goal: term -> int -> term list
    1.13 @@ -508,16 +506,11 @@
    1.14    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
    1.15  
    1.16  val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
    1.17 -val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T);
    1.18  
    1.19  val legacy_varify =
    1.20    Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
    1.21    Term.map_types legacy_varifyT;
    1.22  
    1.23 -val legacy_unvarify =
    1.24 -  Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
    1.25 -  Term.map_types legacy_unvarifyT;
    1.26 -
    1.27  
    1.28  (* goal states *)
    1.29