removed obsolete/unused legacy_varify;
authorwenzelm
Thu Jul 16 00:24:11 2009 +0200 (2009-07-16)
changeset 32014857367925493
parent 32013 5589a5360ddc
child 32015 7101feb5247e
removed obsolete/unused legacy_varify;
src/Pure/logic.ML
     1.1 --- a/src/Pure/logic.ML	Thu Jul 16 00:21:36 2009 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu Jul 16 00:24:11 2009 +0200
     1.3 @@ -70,8 +70,6 @@
     1.4    val unvarifyT: typ -> typ
     1.5    val varify: term -> term
     1.6    val unvarify: term -> term
     1.7 -  val legacy_varifyT: typ -> typ
     1.8 -  val legacy_varify: term -> term
     1.9    val get_goal: term -> int -> term
    1.10    val goal_params: term -> int -> term * term list
    1.11    val prems_of_goal: term -> int -> term list
    1.12 @@ -506,12 +504,6 @@
    1.13    |> perhaps (Term_Subst.map_types_option unvarifyT_option)
    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 -
    1.18 -val legacy_varify =
    1.19 -  Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
    1.20 -  Term.map_types legacy_varifyT;
    1.21 -
    1.22  
    1.23  (* goal states *)
    1.24