removed obsolete adhoc_freeze_vars (may use Variable.import_terms instead);
authorwenzelm
Wed Jul 12 21:19:22 2006 +0200 (2006-07-12)
changeset 20116f2aecd6e58ec
parent 20115 6c2ca3749a80
child 20117 0f7b7bfae82b
removed obsolete adhoc_freeze_vars (may use Variable.import_terms instead);
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Wed Jul 12 21:19:19 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Jul 12 21:19:22 2006 +0200
     1.3 @@ -203,7 +203,6 @@
     1.4    val replace_dummy_patterns: int * term -> int * term
     1.5    val is_replaced_dummy_pattern: indexname -> bool
     1.6    val show_dummy_patterns: term -> term
     1.7 -  val adhoc_freeze_vars: term -> term * string list
     1.8    val string_of_vname: indexname -> string
     1.9    val string_of_vname': indexname -> string
    1.10  end;
    1.11 @@ -1312,17 +1311,6 @@
    1.12    | show_dummy_patterns a = a;
    1.13  
    1.14  
    1.15 -(* adhoc freezing *)
    1.16 -
    1.17 -fun adhoc_freeze_vars tm =
    1.18 -  let
    1.19 -    fun mk_inst (var as Var ((a, i), T)) =
    1.20 -      let val x = a ^ Library.gensym "_" ^ string_of_int i
    1.21 -      in ((var,  Free(x, T)), x) end;
    1.22 -    val (insts, xs) = split_list (map mk_inst (term_vars tm));
    1.23 -  in (subst_atomic insts tm, xs) end;
    1.24 -
    1.25 -
    1.26  (* display variables *)
    1.27  
    1.28  val show_question_marks = ref true;