eliminated obsolete freeze_thaw;
authorwenzelm
Thu Jul 27 15:33:21 2006 +0200 (2006-07-27)
changeset 202387e17d70a9303
parent 20237 5daab2c78b8e
child 20239 620a3f297072
eliminated obsolete freeze_thaw;
TFL/rules.ML
src/Pure/conjunction.ML
     1.1 --- a/TFL/rules.ML	Thu Jul 27 14:21:57 2006 +0200
     1.2 +++ b/TFL/rules.ML	Thu Jul 27 15:33:21 2006 +0200
     1.3 @@ -816,10 +816,11 @@
     1.4  fun prove strict (ptm, tac) =
     1.5    let
     1.6      val {thy, t, ...} = Thm.rep_cterm ptm;
     1.7 -    val result =
     1.8 -      if strict then Goal.prove_global thy [] [] t (K tac)
     1.9 -      else Goal.prove_global thy [] [] t (K tac)
    1.10 -        handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg);
    1.11 -  in #1 (freeze_thaw result) end;
    1.12 +    val ctxt = ProofContext.init thy |> ProofContext.fix_frees t;
    1.13 +  in
    1.14 +    if strict then Goal.prove ctxt [] [] t (K tac)
    1.15 +    else Goal.prove ctxt [] [] t (K tac)
    1.16 +      handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg)
    1.17 +  end;
    1.18  
    1.19  end;
     2.1 --- a/src/Pure/conjunction.ML	Thu Jul 27 14:21:57 2006 +0200
     2.2 +++ b/src/Pure/conjunction.ML	Thu Jul 27 15:33:21 2006 +0200
     2.3 @@ -74,7 +74,7 @@
     2.4  val ABC = read "PROP A ==> PROP B ==> PROP C";
     2.5  val A_B = read "PROP ProtoPure.conjunction(A, B)"
     2.6  
     2.7 -val conjunction_def = #1 (freeze_thaw ProtoPure.conjunction_def);
     2.8 +val conjunction_def = Drule.unvarify ProtoPure.conjunction_def;
     2.9  
    2.10  fun conjunctionD which =
    2.11    Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP