clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;