--- a/src/Pure/ML/ml_thms.ML Thu Apr 07 13:35:08 2016 +0200 +++ b/src/Pure/ML/ml_thms.ML Thu Apr 07 13:54:02 2016 +0200 @@ -138,4 +138,3 @@ fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms); end; -