# HG changeset patch
# User wenzelm
# Date 1272916806 -7200
# Node ID ed80839302039442affa774cdb5e268d412bb0f8
# Parent  712724c32ac80bf047b94c7a2fcba022bdd9e0bd
UNDISCH/DISJ_CASESL: eliminated slightly odd Thm.legacy_freezeT -- these rules appear to be applied to thms with fixed types only;

diff -r 712724c32ac8 -r ed8083930203 src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Mon May 03 20:53:49 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Mon May 03 22:00:06 2010 +0200
@@ -134,9 +134,8 @@
  in  fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm
  end;
 
-(* freezeT expensive! *)
 fun UNDISCH thm =
-   let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.legacy_freezeT thm))))
+   let val tm = D.mk_prop (#1 (D.dest_imp (cconcl thm)))
    in Thm.implies_elim (thm RS mp) (ASSUME tm) end
    handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
      | THM _ => raise RULES_ERR "UNDISCH" "";
@@ -252,7 +251,7 @@
        | place _ _ = raise RULES_ERR "organize" "not a permutation.2"
  in place
  end;
-(* freezeT expensive! *)
+
 fun DISJ_CASESL disjth thl =
    let val c = cconcl disjth
        fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
@@ -265,7 +264,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.legacy_freezeT disjth) (organize eq tml thl)
+   in DL disjth (organize eq tml thl)
    end;