# HG changeset patch # User wenzelm # Date 1247566732 -7200 # Node ID 6ef7056e5215cfc11cbf2c4c23f5a28c70aa4e26 # Parent befec6450fd67b5f6281a9581aead7b797bb60d4 removed obsolete/unused legacy_unvarify; diff -r befec6450fd6 -r 6ef7056e5215 src/Pure/logic.ML --- a/src/Pure/logic.ML Tue Jul 14 12:10:44 2009 +0200 +++ b/src/Pure/logic.ML Tue Jul 14 12:18:52 2009 +0200 @@ -71,9 +71,7 @@ val varify: term -> term val unvarify: term -> term val legacy_varifyT: typ -> typ - val legacy_unvarifyT: typ -> typ val legacy_varify: term -> term - val legacy_unvarify: term -> term val get_goal: term -> int -> term val goal_params: term -> int -> term * term list val prems_of_goal: term -> int -> term list @@ -508,16 +506,11 @@ 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_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T); val legacy_varify = Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #> Term.map_types legacy_varifyT; -val legacy_unvarify = - Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #> - Term.map_types legacy_unvarifyT; - (* goal states *)