# HG changeset patch
# User wenzelm
# Date 869646150 -7200
# Node ID b1013660aeff39d3c9355639d426e13c4ed5fe7e
# Parent  a148c7e7152e2acaff0bee43cd7a3c8de1031316
tuned apsome;

diff -r a148c7e7152e -r b1013660aeff src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue Jul 22 19:33:52 1997 +0200
+++ b/src/Pure/tactic.ML	Wed Jul 23 10:22:30 1997 +0200
@@ -471,9 +471,7 @@
 (*** Meta-Rewriting Tactics ***)
 
 fun result1 tacf mss thm =
-  case Sequence.pull(tacf mss thm) of
-    None => None
-  | Some(thm,_) => Some(thm);
+  apsome fst (Sequence.pull (tacf mss thm));
 
 (*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
 fun asm_rewrite_goal_tac mode prover_tac mss =