src/Pure/ML-Systems/maximum_ml_stack_dummy.ML
changeset 59468 fe6651760643
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/maximum_ml_stack_dummy.ML	Thu Jan 29 15:21:16 2015 +0100
@@ -0,0 +1,7 @@
+(*  Title:      Pure/ML-Systems/maximum_ml_stack_dummy.ML
+
+Maximum stack size (in words) for ML threads -- dummy version.
+*)
+
+fun maximum_ml_stack (_: int option) : Thread.threadAttribute list = [];
+