# HG changeset patch
# User wenzelm
# Date 1150741290 -7200
# Node ID 3f93418318126eaa7e7a9905992dc89feec3db24
# Parent  ee3c4ec1d6528fa79f86dfb079ade1df2f412e12
eliminated freeze/varify in favour of Variable.import/export/trade;

diff -r ee3c4ec1d652 -r 3f9341831812 TFL/post.ML
--- a/TFL/post.ML	Mon Jun 19 19:56:32 2006 +0200
+++ b/TFL/post.ML	Mon Jun 19 20:21:30 2006 +0200
@@ -170,7 +170,9 @@
   | tracing false msg = writeln msg;
 
 fun simplify_defn strict thy cs ss congs wfs id pats def0 =
-   let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
+   let
+       val ([def1], _) = Variable.importT [def0] (Variable.thm_context def0);
+       val def = def1 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)
diff -r ee3c4ec1d652 -r 3f9341831812 TFL/rules.ML
--- a/TFL/rules.ML	Mon Jun 19 19:56:32 2006 +0200
+++ b/TFL/rules.ML	Mon Jun 19 20:21:30 2006 +0200
@@ -137,9 +137,10 @@
               thm (chyps thm)
  end;
 
-(* freezeT expensive! *)
 fun UNDISCH thm =
-   let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm))))
+   let
+     val ([thm'], _) = Variable.importT [thm] (Variable.thm_context thm);
+     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" "";
@@ -253,7 +254,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
@@ -266,8 +267,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
-   in DL (Thm.freezeT disjth) (organize eq tml thl)
-   end;
+       val ([disjth'], _) = Variable.importT [disjth] (Variable.thm_context disjth);
+   in DL disjth' (organize eq tml thl) end;
 
 
 (*----------------------------------------------------------------------------
diff -r ee3c4ec1d652 -r 3f9341831812 TFL/tfl.ML
--- a/TFL/tfl.ML	Mon Jun 19 19:56:32 2006 +0200
+++ b/TFL/tfl.ML	Mon Jun 19 20:21:30 2006 +0200
@@ -555,7 +555,7 @@
        thy
        |> PureThy.add_defs_i false
             [Thm.no_attributes (fid ^ "_def", defn)]
-     val def = Thm.freezeT def0;
+     val ([def], _) = Variable.importT [def0] (Variable.thm_context def0);
      val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
                            else ()
      (* val fconst = #lhs(S.dest_eq(concl def))  *)
diff -r ee3c4ec1d652 -r 3f9341831812 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Mon Jun 19 19:56:32 2006 +0200
+++ b/src/FOLP/simp.ML	Mon Jun 19 20:21:30 2006 +0200
@@ -221,8 +221,9 @@
     in add_norms(congs,ccs,new_asms) end;
 
 fun normed_rews congs =
-  let val add_norms = add_norm_tags congs;
-  in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(Thm.freezeT thm))
+  let val add_norms = add_norm_tags congs in
+    fn thm => Variable.tradeT (Variable.thm_context thm)
+      (map (add_norms o mk_trans) o maps mk_rew_rules) [thm]
   end;
 
 fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];
diff -r ee3c4ec1d652 -r 3f9341831812 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Jun 19 19:56:32 2006 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Mon Jun 19 20:21:30 2006 +0200
@@ -799,7 +799,7 @@
       ||>> apply_theorems [raw_induction];
     val sign = Theory.sign_of thy1;
 
-    val induction' = Thm.freezeT induction;
+    val ([induction'], _) = Variable.importT [induction] (Variable.thm_context induction);
 
     fun err t = error ("Ill-formed predicate in induction rule: " ^
       Sign.string_of_term sign t);
diff -r ee3c4ec1d652 -r 3f9341831812 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon Jun 19 19:56:32 2006 +0200
+++ b/src/Pure/tactic.ML	Mon Jun 19 20:21:30 2006 +0200
@@ -133,12 +133,16 @@
 
 (*Makes a rule by applying a tactic to an existing rule*)
 fun rule_by_tactic tac rl =
-  let val (st, thaw) = freeze_thaw_robust (zero_var_indexes rl)
-  in case Seq.pull (tac st)  of
-        NONE        => raise THM("rule_by_tactic", 0, [rl])
-      | SOME(st',_) => Thm.varifyT (thaw 0 st')
+  let
+    val ctxt = Variable.thm_context rl;
+    val ([st], ctxt') = Variable.import true [rl] ctxt;
+  in
+    (case Seq.pull (tac st) of
+      NONE => raise THM ("rule_by_tactic", 0, [rl])
+    | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st'))
   end;
 
+
 (*** Basic tactics ***)
 
 (*** The following fail if the goal number is out of range: