src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

     (* Is there a repetition? If so, replace later line by earlier one. *)
     else case take_prefix (not o is_same_inference (role, t)) lines of
       (_, []) => line :: lines
     | (pre, Inference_Step (name', _, _, _, _) :: post) =>
       line :: pre @ map (replace_dependencies_in_line (name', [name])) post
-    | _ => raise Fail "unexpected inference"
 
 val waldmeister_conjecture_num = "1.0.0.0"
 
 val repair_waldmeister_endgame =
   let