# HG changeset patch
# User wenzelm
# Date 1152731962 -7200
# Node ID f2aecd6e58ece007bc32e34f89d2ecef48799b1e
# Parent  6c2ca3749a8051a7b70ac86e2e3b8869f5f1fee5
removed obsolete adhoc_freeze_vars (may use Variable.import_terms instead);

diff -r 6c2ca3749a80 -r f2aecd6e58ec src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Jul 12 21:19:19 2006 +0200
+++ b/src/Pure/term.ML	Wed Jul 12 21:19:22 2006 +0200
@@ -203,7 +203,6 @@
   val replace_dummy_patterns: int * term -> int * term
   val is_replaced_dummy_pattern: indexname -> bool
   val show_dummy_patterns: term -> term
-  val adhoc_freeze_vars: term -> term * string list
   val string_of_vname: indexname -> string
   val string_of_vname': indexname -> string
 end;
@@ -1312,17 +1311,6 @@
   | show_dummy_patterns a = a;
 
 
-(* adhoc freezing *)
-
-fun adhoc_freeze_vars tm =
-  let
-    fun mk_inst (var as Var ((a, i), T)) =
-      let val x = a ^ Library.gensym "_" ^ string_of_int i
-      in ((var,  Free(x, T)), x) end;
-    val (insts, xs) = split_list (map mk_inst (term_vars tm));
-  in (subst_atomic insts tm, xs) end;
-
-
 (* display variables *)
 
 val show_question_marks = ref true;