author wenzelm Fri, 20 Mar 2009 11:26:59 +0100 changeset 30606 40a1865ab122 parent 30605 9375e68686cf (current diff) parent 30603 71180005f251 (diff) child 30607 c3d1590debd8 child 30629 5cd9b19edef3 child 30660 53e1b1641f09
merged
```--- a/src/HOLCF/HOLCF.thy	Fri Mar 20 10:44:25 2009 +0100
+++ b/src/HOLCF/HOLCF.thy	Fri Mar 20 11:26:59 2009 +0100
@@ -24,7 +24,8 @@
declaration {* fn _ =>
Simplifier.map_ss (fn simpset => simpset addSolver
(mk_solver' "adm_tac" (fn ss =>
-      Adm.adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
+        (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
*}

end```
```--- a/src/HOLCF/Tools/adm_tac.ML	Fri Mar 20 10:44:25 2009 +0100
+++ b/src/HOLCF/Tools/adm_tac.ML	Fri Mar 20 11:26:59 2009 +0100
@@ -15,7 +15,7 @@

sig
-  val adm_tac: (int -> tactic) -> int -> tactic
+  val adm_tac: Proof.context -> (int -> tactic) -> int -> tactic
end;

@@ -85,14 +85,14 @@
(*** try to prove that terms in list are continuous
if successful, add continuity theorem to list l ***)

-fun prove_cont tac thy s T prems params (ts as ((t, _)::_)) l =
+fun prove_cont ctxt tac s T prems params (ts as ((t, _)::_)) l =  (* FIXME proper context *)
let val parTs = map snd (rev params);
val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
fun mk_all [] t = t
| mk_all ((a,T)::Ts) t = Term.all T \$ (Abs (a, T, mk_all Ts t));
val t = HOLogic.mk_Trueprop (Const (@{const_name cont}, contT) \$ Abs (s, T, t));
val t' = mk_all params (Logic.list_implies (prems, t));
-       val thm = Goal.prove (ProofContext.init thy) [] [] t' (K (tac 1));
+       val thm = Goal.prove ctxt [] [] t' (K (tac 1));
in (ts, thm)::l end
handle ERROR _ => l;

@@ -128,18 +128,18 @@
fun try_dest_adm (Const _ \$ (Const (@{const_name adm}, _) \$ Abs abs)) = SOME abs
| try_dest_adm _ = NONE;

-fun adm_tac tac i state = (i, state) |-> SUBGOAL (fn (goali, _) =>
+fun adm_tac ctxt tac i state = (i, state) |-> SUBGOAL (fn (goali, _) =>
(case try_dest_adm (Logic.strip_assums_concl goali) of
NONE => no_tac
| SOME (s, T, t) =>
let
-        val thy = Thm.theory_of_thm state;
+        val thy = ProofContext.theory_of ctxt;
val prems = Logic.strip_assums_hyp goali;
val params = Logic.strip_params goali;
val ts = find_subterms t 0 [];
val ts' = filter eq_terms ts;
val ts'' = filter (is_chfin thy T params) ts';
-        val thms = fold (prove_cont tac thy s T prems params) ts'' [];
+        val thms = fold (prove_cont ctxt tac s T prems params) ts'' [];
in
(case thms of
((ts as ((t', _)::_), cont_thm) :: _) =>```
```--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Mar 20 10:44:25 2009 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Mar 20 11:26:59 2009 +0100
@@ -77,11 +77,9 @@
fun with_attributes new_atts f x =
let
val orig_atts = safe_interrupts (Thread.getAttributes ());
-    fun restore () = Thread.setAttributes orig_atts;
-    val result =
-      (Thread.setAttributes (safe_interrupts new_atts);
-        Exn.Result (f orig_atts x) before restore ())
-      handle e => Exn.Exn e before restore ();
+    val result = Exn.capture (fn () =>
+      (Thread.setAttributes (safe_interrupts new_atts); f orig_atts x)) ();
+    val _ = Thread.setAttributes orig_atts;
in Exn.release result end;

fun interruptible f = with_attributes regular_interrupts (fn _ => f);```