src/Pure/more_pattern.ML
changeset 67010 cf56dd6f3ad1
parent 59095 3100a7b1c092
child 70443 a21a96eda033
--- 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;
-