diff -r 38507aef93cd -r cff42395c246 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Nov 21 14:03:36 2009 +0100
+++ b/src/Pure/drule.ML	Sat Nov 21 15:49:29 2009 +0100
@@ -21,8 +21,8 @@
   val forall_elim_list: cterm list -> thm -> thm
   val gen_all: thm -> thm
   val lift_all: cterm -> thm -> thm
-  val freeze_thaw: thm -> thm * (thm -> thm)
-  val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
+  val legacy_freeze_thaw: thm -> thm * (thm -> thm)
+  val legacy_freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
   val implies_elim_list: thm -> thm list -> thm
   val implies_intr_list: cterm list -> thm -> thm
   val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
@@ -325,7 +325,7 @@
   reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.
   Similar code in type/freeze_thaw*)
 
-fun freeze_thaw_robust th =
+fun legacy_freeze_thaw_robust th =
  let val fth = Thm.freezeT th
      val thy = Thm.theory_of_thm fth
      val {prop, tpairs, ...} = rep_thm fth
@@ -346,9 +346,8 @@
  end;
 
 (*Basic version of the function above. No option to rename Vars apart in thaw.
-  The Frees created from Vars have nice names. FIXME: does not check for
-  clashes with variables in the assumptions, so delete and use freeze_thaw_robust instead?*)
-fun freeze_thaw th =
+  The Frees created from Vars have nice names.*)
+fun legacy_freeze_thaw th =
  let val fth = Thm.freezeT th
      val thy = Thm.theory_of_thm fth
      val {prop, tpairs, ...} = rep_thm fth