src/Pure/ML/ml_thms.ML
changeset 62900 c641bf9402fd
parent 62876 507c90523113
child 63120 629a4c5e953e
--- 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;
-