--- a/src/Pure/more_pattern.ML Sun Nov 05 12:13:27 2017 +0100 +++ b/src/Pure/more_pattern.ML Sun Nov 05 14:35:43 2017 +0100 @@ -121,4 +121,3 @@ open Pattern; end; -