merged
authorwenzelm
Fri Mar 20 11:26:59 2009 +0100 (2009-03-20)
changeset 3060640a1865ab122
parent 30605 9375e68686cf
parent 30603 71180005f251
child 30607 c3d1590debd8
child 30629 5cd9b19edef3
child 30660 53e1b1641f09
merged
     1.1 --- a/src/HOLCF/HOLCF.thy	Fri Mar 20 10:44:25 2009 +0100
     1.2 +++ b/src/HOLCF/HOLCF.thy	Fri Mar 20 11:26:59 2009 +0100
     1.3 @@ -24,7 +24,8 @@
     1.4  declaration {* fn _ =>
     1.5    Simplifier.map_ss (fn simpset => simpset addSolver
     1.6      (mk_solver' "adm_tac" (fn ss =>
     1.7 -      Adm.adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
     1.8 +      Adm.adm_tac (Simplifier.the_context ss)
     1.9 +        (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
    1.10  *}
    1.11  
    1.12  end
     2.1 --- a/src/HOLCF/Tools/adm_tac.ML	Fri Mar 20 10:44:25 2009 +0100
     2.2 +++ b/src/HOLCF/Tools/adm_tac.ML	Fri Mar 20 11:26:59 2009 +0100
     2.3 @@ -15,7 +15,7 @@
     2.4  
     2.5  signature ADM =
     2.6  sig
     2.7 -  val adm_tac: (int -> tactic) -> int -> tactic
     2.8 +  val adm_tac: Proof.context -> (int -> tactic) -> int -> tactic
     2.9  end;
    2.10  
    2.11  structure Adm: ADM =
    2.12 @@ -85,14 +85,14 @@
    2.13  (*** try to prove that terms in list are continuous
    2.14       if successful, add continuity theorem to list l ***)
    2.15  
    2.16 -fun prove_cont tac thy s T prems params (ts as ((t, _)::_)) l =
    2.17 +fun prove_cont ctxt tac s T prems params (ts as ((t, _)::_)) l =  (* FIXME proper context *)
    2.18    let val parTs = map snd (rev params);
    2.19         val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
    2.20         fun mk_all [] t = t
    2.21           | mk_all ((a,T)::Ts) t = Term.all T $ (Abs (a, T, mk_all Ts t));
    2.22         val t = HOLogic.mk_Trueprop (Const (@{const_name cont}, contT) $ Abs (s, T, t));
    2.23         val t' = mk_all params (Logic.list_implies (prems, t));
    2.24 -       val thm = Goal.prove (ProofContext.init thy) [] [] t' (K (tac 1));
    2.25 +       val thm = Goal.prove ctxt [] [] t' (K (tac 1));
    2.26    in (ts, thm)::l end
    2.27    handle ERROR _ => l;
    2.28  
    2.29 @@ -128,18 +128,18 @@
    2.30  fun try_dest_adm (Const _ $ (Const (@{const_name adm}, _) $ Abs abs)) = SOME abs
    2.31    | try_dest_adm _ = NONE;
    2.32  
    2.33 -fun adm_tac tac i state = (i, state) |-> SUBGOAL (fn (goali, _) =>
    2.34 +fun adm_tac ctxt tac i state = (i, state) |-> SUBGOAL (fn (goali, _) =>
    2.35    (case try_dest_adm (Logic.strip_assums_concl goali) of
    2.36      NONE => no_tac
    2.37    | SOME (s, T, t) =>
    2.38        let
    2.39 -        val thy = Thm.theory_of_thm state;
    2.40 +        val thy = ProofContext.theory_of ctxt;
    2.41          val prems = Logic.strip_assums_hyp goali;
    2.42          val params = Logic.strip_params goali;
    2.43          val ts = find_subterms t 0 [];
    2.44          val ts' = filter eq_terms ts;
    2.45          val ts'' = filter (is_chfin thy T params) ts';
    2.46 -        val thms = fold (prove_cont tac thy s T prems params) ts'' [];
    2.47 +        val thms = fold (prove_cont ctxt tac s T prems params) ts'' [];
    2.48        in
    2.49          (case thms of
    2.50            ((ts as ((t', _)::_), cont_thm) :: _) =>
     3.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Mar 20 10:44:25 2009 +0100
     3.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Mar 20 11:26:59 2009 +0100
     3.3 @@ -77,11 +77,9 @@
     3.4  fun with_attributes new_atts f x =
     3.5    let
     3.6      val orig_atts = safe_interrupts (Thread.getAttributes ());
     3.7 -    fun restore () = Thread.setAttributes orig_atts;
     3.8 -    val result =
     3.9 -      (Thread.setAttributes (safe_interrupts new_atts);
    3.10 -        Exn.Result (f orig_atts x) before restore ())
    3.11 -      handle e => Exn.Exn e before restore ();
    3.12 +    val result = Exn.capture (fn () =>
    3.13 +      (Thread.setAttributes (safe_interrupts new_atts); f orig_atts x)) ();
    3.14 +    val _ = Thread.setAttributes orig_atts;
    3.15    in Exn.release result end;
    3.16  
    3.17  fun interruptible f = with_attributes regular_interrupts (fn _ => f);