changeset 52756 | 1ac8a0d0ddb1 |
parent 52697 | 6fb98a20c349 |
child 53047 | 8dceafa07c4f |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Jul 29 15:42:04 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Jul 29 16:13:35 2013 +0200 @@ -327,8 +327,7 @@ val add_labels_of_proof = steps_of_proof #> fold_isar_steps - (byline_of_step #> (fn SOME (By ((ls, _), _)) => union (op =) ls - | _ => I)) + (byline_of_step #> (fn SOME (By ((ls, _), _)) => union (op =) ls | _ => I)) fun kill_useless_labels_in_proof proof = let