# HG changeset patch
# User wenzelm
# Date 1258814969 -3600
# Node ID cff42395c246f50eb06a40c48472bff967d88f42
# Parent  38507aef93cd1f2e93938647738eb120eb73c27c
explicitly mark some legacy freeze operations;

diff -r 38507aef93cd -r cff42395c246 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Import/shuffler.ML	Sat Nov 21 15:49:29 2009 +0100
@@ -294,7 +294,7 @@
 fun eta_contract thy assumes origt =
     let
         val (typet,Tinst) = freeze_thaw_term origt
-        val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
+        val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet))
         val final = inst_tfrees thy Tinst o thaw
         val t = #1 (Logic.dest_equals (prop_of init))
         val _ =
@@ -357,7 +357,7 @@
 fun eta_expand thy assumes origt =
     let
         val (typet,Tinst) = freeze_thaw_term origt
-        val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
+        val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet))
         val final = inst_tfrees thy Tinst o thaw
         val t = #1 (Logic.dest_equals (prop_of init))
         val _ =
diff -r 38507aef93cd -r cff42395c246 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sat Nov 21 15:49:29 2009 +0100
@@ -365,7 +365,7 @@
       let
         val prop = Thm.prop_of thm;
         val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
-          (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
+          (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.legacy_freeze prop;
         val used = OldTerm.add_term_tfree_names (a, []);
 
         fun mk_thm i =
diff -r 38507aef93cd -r cff42395c246 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Sat Nov 21 15:49:29 2009 +0100
@@ -27,7 +27,7 @@
  * have a tactic directly applied to them.
  *--------------------------------------------------------------------------*)
 fun termination_goals rules =
-    map (Type.freeze o HOLogic.dest_Trueprop)
+    map (Type.legacy_freeze o HOLogic.dest_Trueprop)
       (fold_rev (union (op aconv) o prems_of) rules []);
 
 (*---------------------------------------------------------------------------
diff -r 38507aef93cd -r cff42395c246 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Tools/meson.ML	Sat Nov 21 15:49:29 2009 +0100
@@ -665,7 +665,7 @@
 
 (*Converting one theorem from a disjunction to a meta-level clause*)
 fun make_meta_clause th =
-  let val (fth,thaw) = Drule.freeze_thaw_robust th
+  let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
   in  
       (zero_var_indexes o Thm.varifyT o thaw 0 o 
        negated_asm_of_head o make_horn resolution_clause_rules) fth
diff -r 38507aef93cd -r cff42395c246 src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML	Sat Nov 21 15:49:29 2009 +0100
@@ -45,7 +45,7 @@
       let val consts = map snd (filter (fn (c, _) => c = cname) intr_consts)
       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
     val (env, _) = fold unify rec_consts (Vartab.empty, i');
-    val subst = Type.freeze o map_types (Envir.norm_type env)
+    val subst = Type.legacy_freeze o map_types (Envir.norm_type env)
 
   in (map subst cs', map subst intr_ts')
   end) handle Type.TUNIFY =>
diff -r 38507aef93cd -r cff42395c246 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Sat Nov 21 15:49:29 2009 +0100
@@ -29,8 +29,7 @@
 val trace = Unsynchronized.ref false;
 fun trace_msg msg = if ! trace then tracing (msg ()) else ();
 
-(* FIXME legacy *)
-fun freeze_thm th = #1 (Drule.freeze_thaw th);
+fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
 
 fun type_has_empty_sort (TFree (_, [])) = true
   | type_has_empty_sort (TVar (_, [])) = true
diff -r 38507aef93cd -r cff42395c246 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat Nov 21 14:03:36 2009 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Nov 21 15:49:29 2009 +0100
@@ -310,7 +310,7 @@
       val vars' = filter_out (fn v =>
         member (op =) rtypes (tname_of (body_type (fastype_of v)))) vars;
       val T = etype_of thy' vs [] prop;
-      val (T', thw) = Type.freeze_thaw_type
+      val (T', thw) = Type.legacy_freeze_thaw_type
         (if T = nullT then nullT else map fastype_of vars' ---> T);
       val t = map_types thw (OldGoals.simple_read_term thy' T' s1);
       val r' = freeze_thaw (condrew thy' eqns
@@ -720,8 +720,8 @@
          NONE =>
            let
              val corr_prop = Reconstruct.prop_of prf;
-             val ft = Type.freeze t;
-             val fu = Type.freeze u;
+             val ft = Type.legacy_freeze t;
+             val fu = Type.legacy_freeze u;
              val (def_thms, thy') = if t = nullt then ([], thy) else
                thy
                |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
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
diff -r 38507aef93cd -r cff42395c246 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Nov 21 14:03:36 2009 +0100
+++ b/src/Pure/thm.ML	Sat Nov 21 15:49:29 2009 +0100
@@ -1267,7 +1267,7 @@
 fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
   let
     val prop1 = attach_tpairs tpairs prop;
-    val prop2 = Type.freeze prop1;
+    val prop2 = Type.legacy_freeze prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   in
     Thm (deriv_rule1 (Pt.freezeT prop1) der,
diff -r 38507aef93cd -r cff42395c246 src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Nov 21 14:03:36 2009 +0100
+++ b/src/Pure/type.ML	Sat Nov 21 15:49:29 2009 +0100
@@ -44,10 +44,10 @@
   val strip_sorts: typ -> typ
   val no_tvars: typ -> typ
   val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term
-  val freeze_thaw_type: typ -> typ * (typ -> typ)
-  val freeze_type: typ -> typ
-  val freeze_thaw: term -> term * (term -> term)
-  val freeze: term -> term
+  val legacy_freeze_thaw_type: typ -> typ * (typ -> typ)
+  val legacy_freeze_type: typ -> typ
+  val legacy_freeze_thaw: term -> term * (term -> term)
+  val legacy_freeze: term -> term
 
   (*matching and unification*)
   exception TYPE_MATCH
@@ -277,17 +277,16 @@
 
 in
 
-(*this sort of code could replace unvarifyT*)
-fun freeze_thaw_type T =
+fun legacy_freeze_thaw_type T =
   let
     val used = OldTerm.add_typ_tfree_names (T, [])
     and tvars = map #1 (OldTerm.add_typ_tvars (T, []));
     val (alist, _) = List.foldr new_name ([], used) tvars;
   in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
 
-val freeze_type = #1 o freeze_thaw_type;
+val legacy_freeze_type = #1 o legacy_freeze_thaw_type;
 
-fun freeze_thaw t =
+fun legacy_freeze_thaw t =
   let
     val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
     and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
@@ -299,7 +298,7 @@
       map_types (map_type_tfree (thaw_one (map swap alist)))))
   end;
 
-val freeze = #1 o freeze_thaw;
+val legacy_freeze = #1 o legacy_freeze_thaw;
 
 end;