# HG changeset patch # User wenzelm # Date 1272910416 -7200 # Node ID 88756a5a92fc8cfc7d88bd0d08863ca2864f5f91 # Parent b6c031ad3690adaf04ddf7b781dec53efbed5e95 renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze; diff -r b6c031ad3690 -r 88756a5a92fc src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Mon May 03 16:26:47 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon May 03 20:13:36 2010 +0200 @@ -48,7 +48,7 @@ fun atomize_thm thm = let - val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *) + val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *) val thm'' = Object_Logic.atomize (cprop_of thm') in @{thm equal_elim_rule1} OF [thm'', thm'] diff -r b6c031ad3690 -r 88756a5a92fc src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Mon May 03 16:26:47 2010 +0200 +++ b/src/HOL/Tools/TFL/post.ML Mon May 03 20:13:36 2010 +0200 @@ -141,7 +141,7 @@ fun simplify_defn strict thy cs ss congs wfs id pats def0 = let val ctxt = ProofContext.init_global thy - val def = Thm.freezeT def0 RS meta_eq_to_obj_eq + val def = Thm.legacy_freezeT def0 RS meta_eq_to_obj_eq val {rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats)) val {lhs=f,rhs} = S.dest_eq (concl def) diff -r b6c031ad3690 -r 88756a5a92fc src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Mon May 03 16:26:47 2010 +0200 +++ b/src/HOL/Tools/TFL/rules.ML Mon May 03 20:13:36 2010 +0200 @@ -136,7 +136,7 @@ (* freezeT expensive! *) fun UNDISCH thm = - let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm)))) + let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.legacy_freezeT thm)))) in Thm.implies_elim (thm RS mp) (ASSUME tm) end handle U.ERR _ => raise RULES_ERR "UNDISCH" "" | THM _ => raise RULES_ERR "UNDISCH" ""; @@ -265,7 +265,7 @@ | DL th (th1::rst) = let val tm = #2(D.dest_disj(D.drop_prop(cconcl th))) in DISJ_CASES th th1 (DL (ASSUME tm) rst) end - in DL (Thm.freezeT disjth) (organize eq tml thl) + in DL (Thm.legacy_freezeT disjth) (organize eq tml thl) end; diff -r b6c031ad3690 -r 88756a5a92fc src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Mon May 03 16:26:47 2010 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Mon May 03 20:13:36 2010 +0200 @@ -541,7 +541,7 @@ thy |> PureThy.add_defs false [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)] - val def = Thm.freezeT def0; + val def = Thm.legacy_freezeT def0; val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def) else () diff -r b6c031ad3690 -r 88756a5a92fc src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Mon May 03 16:26:47 2010 +0200 +++ b/src/HOL/Tools/choice_specification.ML Mon May 03 20:13:36 2010 +0200 @@ -79,7 +79,7 @@ end fun add_specification axiomatic cos arg = - arg |> apsnd Thm.freezeT + arg |> apsnd Thm.legacy_freezeT |> proc_exprop axiomatic cos |> apsnd Drule.export_without_context @@ -217,7 +217,7 @@ then writeln "specification" else () in - arg |> apsnd Thm.freezeT + arg |> apsnd Thm.legacy_freezeT |> process_all (zip3 alt_names rew_imps frees) end diff -r b6c031ad3690 -r 88756a5a92fc src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Mon May 03 16:26:47 2010 +0200 +++ b/src/Pure/Isar/code.ML Mon May 03 20:13:36 2010 +0200 @@ -778,7 +778,7 @@ val _ = if c = const_abs_eqn thy abs_thm then () else error ("Wrong head of abstract code equation,\nexpected constant " ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm); - in Abstract (Thm.freezeT abs_thm, tyco) end; + in Abstract (Thm.legacy_freezeT abs_thm, tyco) end; fun constrain_cert thy sorts (Equations (cert_thm, propers)) = let diff -r b6c031ad3690 -r 88756a5a92fc src/Pure/drule.ML --- a/src/Pure/drule.ML Mon May 03 16:26:47 2010 +0200 +++ b/src/Pure/drule.ML Mon May 03 20:13:36 2010 +0200 @@ -307,7 +307,7 @@ Similar code in type/freeze_thaw*) fun legacy_freeze_thaw_robust th = - let val fth = Thm.freezeT th + let val fth = Thm.legacy_freezeT th val thy = Thm.theory_of_thm fth val {prop, tpairs, ...} = rep_thm fth in @@ -329,7 +329,7 @@ (*Basic version of the function above. No option to rename Vars apart in thaw. The Frees created from Vars have nice names.*) fun legacy_freeze_thaw th = - let val fth = Thm.freezeT th + let val fth = Thm.legacy_freezeT th val thy = Thm.theory_of_thm fth val {prop, tpairs, ...} = rep_thm fth in diff -r b6c031ad3690 -r 88756a5a92fc src/Pure/thm.ML --- a/src/Pure/thm.ML Mon May 03 16:26:47 2010 +0200 +++ b/src/Pure/thm.ML Mon May 03 20:13:36 2010 +0200 @@ -140,7 +140,7 @@ val strip_shyps: thm -> thm val unconstrainT: ctyp -> thm -> thm val unconstrain_allTs: thm -> thm - val freezeT: thm -> thm + val legacy_freezeT: thm -> thm val assumption: int -> thm -> thm Seq.seq val eq_assumption: int -> thm -> thm val rotate_rule: int -> int -> thm -> thm @@ -1261,8 +1261,8 @@ val varifyT_global = #2 o varifyT_global' []; -(* Replace all TVars by new TFrees *) -fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) = +(* Replace all TVars by TFrees that are often new *) +fun legacy_freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) = let val prop1 = attach_tpairs tpairs prop; val prop2 = Type.legacy_freeze prop1; diff -r b6c031ad3690 -r 88756a5a92fc src/Tools/nbe.ML --- a/src/Tools/nbe.ML Mon May 03 16:26:47 2010 +0200 +++ b/src/Tools/nbe.ML Mon May 03 20:13:36 2010 +0200 @@ -105,14 +105,14 @@ |> Drule.cterm_rule Thm.varifyT_global |> Thm.instantiate_cterm (Thm.certify_inst thy (map (fn (v, ((sort, _), sort')) => (((v, 0), sort), TFree (v, sort'))) vs, [])) - |> Drule.cterm_rule Thm.freezeT + |> Drule.cterm_rule Thm.legacy_freezeT |> conv |> Thm.varifyT_global |> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs |> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) => (((v, 0), []), TVar ((v, 0), sort))) vs, []) |> strip_of_class - |> Thm.freezeT + |> Thm.legacy_freezeT end; fun lift_triv_classes_rew thy rew t =