explicitly mark some legacy freeze operations;
authorwenzelm
Sat Nov 21 15:49:29 2009 +0100 (2009-11-21)
changeset 33832cff42395c246
parent 33831 38507aef93cd
child 33833 c38c2a1883e7
explicitly mark some legacy freeze operations;
src/HOL/Import/shuffler.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/res_axioms.ML
src/Pure/Proof/extraction.ML
src/Pure/drule.ML
src/Pure/thm.ML
src/Pure/type.ML
     1.1 --- a/src/HOL/Import/shuffler.ML	Sat Nov 21 14:03:36 2009 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Sat Nov 21 15:49:29 2009 +0100
     1.3 @@ -294,7 +294,7 @@
     1.4  fun eta_contract thy assumes origt =
     1.5      let
     1.6          val (typet,Tinst) = freeze_thaw_term origt
     1.7 -        val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
     1.8 +        val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet))
     1.9          val final = inst_tfrees thy Tinst o thaw
    1.10          val t = #1 (Logic.dest_equals (prop_of init))
    1.11          val _ =
    1.12 @@ -357,7 +357,7 @@
    1.13  fun eta_expand thy assumes origt =
    1.14      let
    1.15          val (typet,Tinst) = freeze_thaw_term origt
    1.16 -        val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
    1.17 +        val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet))
    1.18          val final = inst_tfrees thy Tinst o thaw
    1.19          val t = #1 (Logic.dest_equals (prop_of init))
    1.20          val _ =
     2.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sat Nov 21 14:03:36 2009 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sat Nov 21 15:49:29 2009 +0100
     2.3 @@ -365,7 +365,7 @@
     2.4        let
     2.5          val prop = Thm.prop_of thm;
     2.6          val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
     2.7 -          (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
     2.8 +          (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.legacy_freeze prop;
     2.9          val used = OldTerm.add_term_tfree_names (a, []);
    2.10  
    2.11          fun mk_thm i =
     3.1 --- a/src/HOL/Tools/TFL/post.ML	Sat Nov 21 14:03:36 2009 +0100
     3.2 +++ b/src/HOL/Tools/TFL/post.ML	Sat Nov 21 15:49:29 2009 +0100
     3.3 @@ -27,7 +27,7 @@
     3.4   * have a tactic directly applied to them.
     3.5   *--------------------------------------------------------------------------*)
     3.6  fun termination_goals rules =
     3.7 -    map (Type.freeze o HOLogic.dest_Trueprop)
     3.8 +    map (Type.legacy_freeze o HOLogic.dest_Trueprop)
     3.9        (fold_rev (union (op aconv) o prems_of) rules []);
    3.10  
    3.11  (*---------------------------------------------------------------------------
     4.1 --- a/src/HOL/Tools/meson.ML	Sat Nov 21 14:03:36 2009 +0100
     4.2 +++ b/src/HOL/Tools/meson.ML	Sat Nov 21 15:49:29 2009 +0100
     4.3 @@ -665,7 +665,7 @@
     4.4  
     4.5  (*Converting one theorem from a disjunction to a meta-level clause*)
     4.6  fun make_meta_clause th =
     4.7 -  let val (fth,thaw) = Drule.freeze_thaw_robust th
     4.8 +  let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
     4.9    in  
    4.10        (zero_var_indexes o Thm.varifyT o thaw 0 o 
    4.11         negated_asm_of_head o make_horn resolution_clause_rules) fth
     5.1 --- a/src/HOL/Tools/old_primrec.ML	Sat Nov 21 14:03:36 2009 +0100
     5.2 +++ b/src/HOL/Tools/old_primrec.ML	Sat Nov 21 15:49:29 2009 +0100
     5.3 @@ -45,7 +45,7 @@
     5.4        let val consts = map snd (filter (fn (c, _) => c = cname) intr_consts)
     5.5        in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
     5.6      val (env, _) = fold unify rec_consts (Vartab.empty, i');
     5.7 -    val subst = Type.freeze o map_types (Envir.norm_type env)
     5.8 +    val subst = Type.legacy_freeze o map_types (Envir.norm_type env)
     5.9  
    5.10    in (map subst cs', map subst intr_ts')
    5.11    end) handle Type.TUNIFY =>
     6.1 --- a/src/HOL/Tools/res_axioms.ML	Sat Nov 21 14:03:36 2009 +0100
     6.2 +++ b/src/HOL/Tools/res_axioms.ML	Sat Nov 21 15:49:29 2009 +0100
     6.3 @@ -29,8 +29,7 @@
     6.4  val trace = Unsynchronized.ref false;
     6.5  fun trace_msg msg = if ! trace then tracing (msg ()) else ();
     6.6  
     6.7 -(* FIXME legacy *)
     6.8 -fun freeze_thm th = #1 (Drule.freeze_thaw th);
     6.9 +fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
    6.10  
    6.11  fun type_has_empty_sort (TFree (_, [])) = true
    6.12    | type_has_empty_sort (TVar (_, [])) = true
     7.1 --- a/src/Pure/Proof/extraction.ML	Sat Nov 21 14:03:36 2009 +0100
     7.2 +++ b/src/Pure/Proof/extraction.ML	Sat Nov 21 15:49:29 2009 +0100
     7.3 @@ -310,7 +310,7 @@
     7.4        val vars' = filter_out (fn v =>
     7.5          member (op =) rtypes (tname_of (body_type (fastype_of v)))) vars;
     7.6        val T = etype_of thy' vs [] prop;
     7.7 -      val (T', thw) = Type.freeze_thaw_type
     7.8 +      val (T', thw) = Type.legacy_freeze_thaw_type
     7.9          (if T = nullT then nullT else map fastype_of vars' ---> T);
    7.10        val t = map_types thw (OldGoals.simple_read_term thy' T' s1);
    7.11        val r' = freeze_thaw (condrew thy' eqns
    7.12 @@ -720,8 +720,8 @@
    7.13           NONE =>
    7.14             let
    7.15               val corr_prop = Reconstruct.prop_of prf;
    7.16 -             val ft = Type.freeze t;
    7.17 -             val fu = Type.freeze u;
    7.18 +             val ft = Type.legacy_freeze t;
    7.19 +             val fu = Type.legacy_freeze u;
    7.20               val (def_thms, thy') = if t = nullt then ([], thy) else
    7.21                 thy
    7.22                 |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
     8.1 --- a/src/Pure/drule.ML	Sat Nov 21 14:03:36 2009 +0100
     8.2 +++ b/src/Pure/drule.ML	Sat Nov 21 15:49:29 2009 +0100
     8.3 @@ -21,8 +21,8 @@
     8.4    val forall_elim_list: cterm list -> thm -> thm
     8.5    val gen_all: thm -> thm
     8.6    val lift_all: cterm -> thm -> thm
     8.7 -  val freeze_thaw: thm -> thm * (thm -> thm)
     8.8 -  val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
     8.9 +  val legacy_freeze_thaw: thm -> thm * (thm -> thm)
    8.10 +  val legacy_freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
    8.11    val implies_elim_list: thm -> thm list -> thm
    8.12    val implies_intr_list: cterm list -> thm -> thm
    8.13    val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
    8.14 @@ -325,7 +325,7 @@
    8.15    reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.
    8.16    Similar code in type/freeze_thaw*)
    8.17  
    8.18 -fun freeze_thaw_robust th =
    8.19 +fun legacy_freeze_thaw_robust th =
    8.20   let val fth = Thm.freezeT th
    8.21       val thy = Thm.theory_of_thm fth
    8.22       val {prop, tpairs, ...} = rep_thm fth
    8.23 @@ -346,9 +346,8 @@
    8.24   end;
    8.25  
    8.26  (*Basic version of the function above. No option to rename Vars apart in thaw.
    8.27 -  The Frees created from Vars have nice names. FIXME: does not check for
    8.28 -  clashes with variables in the assumptions, so delete and use freeze_thaw_robust instead?*)
    8.29 -fun freeze_thaw th =
    8.30 +  The Frees created from Vars have nice names.*)
    8.31 +fun legacy_freeze_thaw th =
    8.32   let val fth = Thm.freezeT th
    8.33       val thy = Thm.theory_of_thm fth
    8.34       val {prop, tpairs, ...} = rep_thm fth
     9.1 --- a/src/Pure/thm.ML	Sat Nov 21 14:03:36 2009 +0100
     9.2 +++ b/src/Pure/thm.ML	Sat Nov 21 15:49:29 2009 +0100
     9.3 @@ -1267,7 +1267,7 @@
     9.4  fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
     9.5    let
     9.6      val prop1 = attach_tpairs tpairs prop;
     9.7 -    val prop2 = Type.freeze prop1;
     9.8 +    val prop2 = Type.legacy_freeze prop1;
     9.9      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
    9.10    in
    9.11      Thm (deriv_rule1 (Pt.freezeT prop1) der,
    10.1 --- a/src/Pure/type.ML	Sat Nov 21 14:03:36 2009 +0100
    10.2 +++ b/src/Pure/type.ML	Sat Nov 21 15:49:29 2009 +0100
    10.3 @@ -44,10 +44,10 @@
    10.4    val strip_sorts: typ -> typ
    10.5    val no_tvars: typ -> typ
    10.6    val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term
    10.7 -  val freeze_thaw_type: typ -> typ * (typ -> typ)
    10.8 -  val freeze_type: typ -> typ
    10.9 -  val freeze_thaw: term -> term * (term -> term)
   10.10 -  val freeze: term -> term
   10.11 +  val legacy_freeze_thaw_type: typ -> typ * (typ -> typ)
   10.12 +  val legacy_freeze_type: typ -> typ
   10.13 +  val legacy_freeze_thaw: term -> term * (term -> term)
   10.14 +  val legacy_freeze: term -> term
   10.15  
   10.16    (*matching and unification*)
   10.17    exception TYPE_MATCH
   10.18 @@ -277,17 +277,16 @@
   10.19  
   10.20  in
   10.21  
   10.22 -(*this sort of code could replace unvarifyT*)
   10.23 -fun freeze_thaw_type T =
   10.24 +fun legacy_freeze_thaw_type T =
   10.25    let
   10.26      val used = OldTerm.add_typ_tfree_names (T, [])
   10.27      and tvars = map #1 (OldTerm.add_typ_tvars (T, []));
   10.28      val (alist, _) = List.foldr new_name ([], used) tvars;
   10.29    in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
   10.30  
   10.31 -val freeze_type = #1 o freeze_thaw_type;
   10.32 +val legacy_freeze_type = #1 o legacy_freeze_thaw_type;
   10.33  
   10.34 -fun freeze_thaw t =
   10.35 +fun legacy_freeze_thaw t =
   10.36    let
   10.37      val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
   10.38      and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
   10.39 @@ -299,7 +298,7 @@
   10.40        map_types (map_type_tfree (thaw_one (map swap alist)))))
   10.41    end;
   10.42  
   10.43 -val freeze = #1 o freeze_thaw;
   10.44 +val legacy_freeze = #1 o legacy_freeze_thaw;
   10.45  
   10.46  end;
   10.47