refrain from reforming TFL -- back to previous revision;

--- a/TFL/post.ML	Mon Jun 19 20:21:32 2006 +0200
+++ b/TFL/post.ML	Mon Jun 19 22:06:36 2006 +0200
@@ -170,9 +170,7 @@
   | tracing false msg = writeln msg;
 
 fun simplify_defn strict thy cs ss congs wfs id pats def0 =
-   let
-       val ([def1], _) = Variable.importT [def0] (Variable.thm_context def0);
-       val def = def1 RS meta_eq_to_obj_eq;
+   let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
        val {theory,rules,rows,TCs,full_pats_TCs} =
            Prim.post_definition congs (thy, (def,pats))
        val {lhs=f,rhs} = S.dest_eq (concl def)

--- a/TFL/rules.ML	Mon Jun 19 20:21:32 2006 +0200
+++ b/TFL/rules.ML	Mon Jun 19 22:06:36 2006 +0200
@@ -137,10 +137,9 @@
               thm (chyps thm)
  end;
 
+(* freezeT expensive! *)
 fun UNDISCH thm =
-   let
-     val ([thm'], _) = Variable.importT [thm] (Variable.thm_context thm);
-     val tm = D.mk_prop (#1 (D.dest_imp (cconcl thm')))
+   let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm))))
    in Thm.implies_elim (thm RS mp) (ASSUME tm) end
    handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
      | THM _ => raise RULES_ERR "UNDISCH" "";
@@ -254,7 +253,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
@@ -267,8 +266,8 @@
          | 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
-       val ([disjth'], _) = Variable.importT [disjth] (Variable.thm_context disjth);
-   in DL disjth' (organize eq tml thl) end;
+   in DL (Thm.freezeT disjth) (organize eq tml thl)
+   end;
 
 
 (*----------------------------------------------------------------------------

--- a/TFL/tfl.ML	Mon Jun 19 20:21:32 2006 +0200
+++ b/TFL/tfl.ML	Mon Jun 19 22:06:36 2006 +0200
@@ -555,7 +555,7 @@
        thy
        |> PureThy.add_defs_i false
             [Thm.no_attributes (fid ^ "_def", defn)]
-     val ([def], _) = Variable.importT [def0] (Variable.thm_context def0);
+     val def = Thm.freezeT def0;
      val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
                            else ()
      (* val fconst = #lhs(S.dest_eq(concl def))  *)