# HG changeset patch
# User wenzelm
# Date 1247696651 -7200
# Node ID 8573679254933d2b611c0577e729da747dc6a6e1
# Parent  5589a5360ddc0e7206610de8763cd42915e14986
removed obsolete/unused legacy_varify;

diff -r 5589a5360ddc -r 857367925493 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu Jul 16 00:21:36 2009 +0200
+++ b/src/Pure/logic.ML	Thu Jul 16 00:24:11 2009 +0200
@@ -70,8 +70,6 @@
   val unvarifyT: typ -> typ
   val varify: term -> term
   val unvarify: term -> term
-  val legacy_varifyT: typ -> typ
-  val legacy_varify: term -> term
   val get_goal: term -> int -> term
   val goal_params: term -> int -> term * term list
   val prems_of_goal: term -> int -> term list
@@ -506,12 +504,6 @@
   |> perhaps (Term_Subst.map_types_option unvarifyT_option)
   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
-val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
-
-val legacy_varify =
-  Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
-  Term.map_types legacy_varifyT;
-
 
 (* goal states *)