anchor.diff:  let solve (goal : goal) (solution : term) : tac<unit> =
       bind (trysolve goal solution) (fun b ->
       if b
  -    then __dismiss
  +    then bind __dismiss (fun () -> remove_solved_goals)
       else fail (BU.format3 "%s does not solve %s : %s"
                 (tts (goal_env goal) solution)
                 (tts (goal_env goal) (goal_witness goal))
                 (tts (goal_env goal) (goal_type goal))))
  +
  +let solve' (goal : goal) (solution : term) : tac<unit> =
  +    bind (set_solution goal solution) (fun () ->
  +    bind __dismiss (fun () ->
  +    remove_solved_goals))
   
   let dismiss_all : tac<unit> =
       bind get (fun p ->
  
positive.code:             bind (do_unify (goal_env g) l r) (fun b ->
              if not b
              then fail2 "trefl: not a trivial equality (%s vs %s)" (tts (goal_env g) l) (tts (goal_env g) r)
              else solve g U.exp_unit)
          | hd, _ ->
              fail1 "trefl: not an equality (%s)" (tts (goal_env g) t)
          end
  
negative.code:     bind get      (fun rp' ->
      let p' = {p with goals=lp'.goals@rp'.goals; smt_goals=lp'.smt_goals@rp'.smt_goals@p.smt_goals} in
      bind (set p') (fun _ ->
      bind remove_solved_goals (fun () ->
      ret (a, b)))))))))))
  
  (* focus: runs f on the current goal only, and then restores all the goals *)
  (* There is a user defined version as well, we just use this one internally, but can't mark it as private *)
  