eliminated freeze/varify in favour of Variable.import/export/trade;
authorwenzelm
Mon Jun 19 20:21:30 2006 +0200 (2006-06-19)
changeset 199253f9341831812
parent 19924 ee3c4ec1d652
child 19926 feb4d150cfd8
eliminated freeze/varify in favour of Variable.import/export/trade;
TFL/post.ML
TFL/rules.ML
TFL/tfl.ML
src/FOLP/simp.ML
src/HOL/Tools/datatype_package.ML
src/Pure/tactic.ML
     1.1 --- a/TFL/post.ML	Mon Jun 19 19:56:32 2006 +0200
     1.2 +++ b/TFL/post.ML	Mon Jun 19 20:21:30 2006 +0200
     1.3 @@ -170,7 +170,9 @@
     1.4    | tracing false msg = writeln msg;
     1.5  
     1.6  fun simplify_defn strict thy cs ss congs wfs id pats def0 =
     1.7 -   let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
     1.8 +   let
     1.9 +       val ([def1], _) = Variable.importT [def0] (Variable.thm_context def0);
    1.10 +       val def = def1 RS meta_eq_to_obj_eq;
    1.11         val {theory,rules,rows,TCs,full_pats_TCs} =
    1.12             Prim.post_definition congs (thy, (def,pats))
    1.13         val {lhs=f,rhs} = S.dest_eq (concl def)
     2.1 --- a/TFL/rules.ML	Mon Jun 19 19:56:32 2006 +0200
     2.2 +++ b/TFL/rules.ML	Mon Jun 19 20:21:30 2006 +0200
     2.3 @@ -137,9 +137,10 @@
     2.4                thm (chyps thm)
     2.5   end;
     2.6  
     2.7 -(* freezeT expensive! *)
     2.8  fun UNDISCH thm =
     2.9 -   let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm))))
    2.10 +   let
    2.11 +     val ([thm'], _) = Variable.importT [thm] (Variable.thm_context thm);
    2.12 +     val tm = D.mk_prop (#1 (D.dest_imp (cconcl thm')))
    2.13     in Thm.implies_elim (thm RS mp) (ASSUME tm) end
    2.14     handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
    2.15       | THM _ => raise RULES_ERR "UNDISCH" "";
    2.16 @@ -253,7 +254,7 @@
    2.17         | place _ _ = raise RULES_ERR "organize" "not a permutation.2"
    2.18   in place
    2.19   end;
    2.20 -(* freezeT expensive! *)
    2.21 +
    2.22  fun DISJ_CASESL disjth thl =
    2.23     let val c = cconcl disjth
    2.24         fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
    2.25 @@ -266,8 +267,8 @@
    2.26           | DL th (th1::rst) =
    2.27              let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
    2.28               in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
    2.29 -   in DL (Thm.freezeT disjth) (organize eq tml thl)
    2.30 -   end;
    2.31 +       val ([disjth'], _) = Variable.importT [disjth] (Variable.thm_context disjth);
    2.32 +   in DL disjth' (organize eq tml thl) end;
    2.33  
    2.34  
    2.35  (*----------------------------------------------------------------------------
     3.1 --- a/TFL/tfl.ML	Mon Jun 19 19:56:32 2006 +0200
     3.2 +++ b/TFL/tfl.ML	Mon Jun 19 20:21:30 2006 +0200
     3.3 @@ -555,7 +555,7 @@
     3.4         thy
     3.5         |> PureThy.add_defs_i false
     3.6              [Thm.no_attributes (fid ^ "_def", defn)]
     3.7 -     val def = Thm.freezeT def0;
     3.8 +     val ([def], _) = Variable.importT [def0] (Variable.thm_context def0);
     3.9       val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
    3.10                             else ()
    3.11       (* val fconst = #lhs(S.dest_eq(concl def))  *)
     4.1 --- a/src/FOLP/simp.ML	Mon Jun 19 19:56:32 2006 +0200
     4.2 +++ b/src/FOLP/simp.ML	Mon Jun 19 20:21:30 2006 +0200
     4.3 @@ -221,8 +221,9 @@
     4.4      in add_norms(congs,ccs,new_asms) end;
     4.5  
     4.6  fun normed_rews congs =
     4.7 -  let val add_norms = add_norm_tags congs;
     4.8 -  in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(Thm.freezeT thm))
     4.9 +  let val add_norms = add_norm_tags congs in
    4.10 +    fn thm => Variable.tradeT (Variable.thm_context thm)
    4.11 +      (map (add_norms o mk_trans) o maps mk_rew_rules) [thm]
    4.12    end;
    4.13  
    4.14  fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];
     5.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Jun 19 19:56:32 2006 +0200
     5.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Jun 19 20:21:30 2006 +0200
     5.3 @@ -799,7 +799,7 @@
     5.4        ||>> apply_theorems [raw_induction];
     5.5      val sign = Theory.sign_of thy1;
     5.6  
     5.7 -    val induction' = Thm.freezeT induction;
     5.8 +    val ([induction'], _) = Variable.importT [induction] (Variable.thm_context induction);
     5.9  
    5.10      fun err t = error ("Ill-formed predicate in induction rule: " ^
    5.11        Sign.string_of_term sign t);
     6.1 --- a/src/Pure/tactic.ML	Mon Jun 19 19:56:32 2006 +0200
     6.2 +++ b/src/Pure/tactic.ML	Mon Jun 19 20:21:30 2006 +0200
     6.3 @@ -133,12 +133,16 @@
     6.4  
     6.5  (*Makes a rule by applying a tactic to an existing rule*)
     6.6  fun rule_by_tactic tac rl =
     6.7 -  let val (st, thaw) = freeze_thaw_robust (zero_var_indexes rl)
     6.8 -  in case Seq.pull (tac st)  of
     6.9 -        NONE        => raise THM("rule_by_tactic", 0, [rl])
    6.10 -      | SOME(st',_) => Thm.varifyT (thaw 0 st')
    6.11 +  let
    6.12 +    val ctxt = Variable.thm_context rl;
    6.13 +    val ([st], ctxt') = Variable.import true [rl] ctxt;
    6.14 +  in
    6.15 +    (case Seq.pull (tac st) of
    6.16 +      NONE => raise THM ("rule_by_tactic", 0, [rl])
    6.17 +    | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st'))
    6.18    end;
    6.19  
    6.20 +
    6.21  (*** Basic tactics ***)
    6.22  
    6.23  (*** The following fail if the goal number is out of range: