src/Pure/tactic.ML
changeset 3554 b1013660aeff
parent 3538 ed9de44032e0
child 3575 4e9beacb5339
     1.1 --- a/src/Pure/tactic.ML	Tue Jul 22 19:33:52 1997 +0200
     1.2 +++ b/src/Pure/tactic.ML	Wed Jul 23 10:22:30 1997 +0200
     1.3 @@ -471,9 +471,7 @@
     1.4  (*** Meta-Rewriting Tactics ***)
     1.5  
     1.6  fun result1 tacf mss thm =
     1.7 -  case Sequence.pull(tacf mss thm) of
     1.8 -    None => None
     1.9 -  | Some(thm,_) => Some(thm);
    1.10 +  apsome fst (Sequence.pull (tacf mss thm));
    1.11  
    1.12  (*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
    1.13  fun asm_rewrite_goal_tac mode prover_tac mss =