src/Pure/more_pattern.ML
changeset 67010 cf56dd6f3ad1
parent 59095 3100a7b1c092
     1.1 --- a/src/Pure/more_pattern.ML	Sun Nov 05 12:13:27 2017 +0100
     1.2 +++ b/src/Pure/more_pattern.ML	Sun Nov 05 14:35:43 2017 +0100
     1.3 @@ -121,4 +121,3 @@
     1.4  open Pattern;
     1.5  
     1.6  end;
     1.7 -