# HG changeset patch # User wenzelm # Date 1450908796 -3600 # Node ID 17ba31a2303b970b0656021d0f74e74d6537c7c8 # Parent ab52f183f020289ab90af78492c08cdc46c21d38 tuned; diff -r ab52f183f020 -r 17ba31a2303b src/Pure/ROOT --- a/src/Pure/ROOT Wed Dec 23 23:09:13 2015 +0100 +++ b/src/Pure/ROOT Wed Dec 23 23:13:16 2015 +0100 @@ -27,7 +27,6 @@ "RAW/overloading_smlnj.ML" "RAW/polyml-5.5.2.ML" "RAW/polyml-5.6.ML" - "RAW/polyml-5.6.ML" "RAW/polyml.ML" "RAW/pp_dummy.ML" "RAW/proper_int.ML"