1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 13:04:03 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 14:10:51 2013 +0100
     1.3 @@ -375,7 +375,6 @@
     1.4        (_, []) => line :: lines
     1.5      | (pre, Inference_Step (name', _, _, _, _) :: post) =>
     1.6        line :: pre @ map (replace_dependencies_in_line (name', [name])) post
     1.7 -    | _ => raise Fail "unexpected inference"
     1.8  
     1.9  val waldmeister_conjecture_num = "1.0.0.0"
    1.10