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