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 =