--- 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