src/Pure/General/long_name.ML
changeset 65358 e345e9420109
parent 59916 f673ce6b1e2b
     1.1 --- a/src/Pure/General/long_name.ML	Mon Apr 03 13:39:13 2017 +0200
     1.2 +++ b/src/Pure/General/long_name.ML	Mon Apr 03 14:29:44 2017 +0200
     1.3 @@ -64,4 +64,3 @@
     1.4        in implode (nth_map (length names - 1) f names) end;
     1.5  
     1.6  end;
     1.7 -