Nominal/nominal_function_common.ML
2012-02-16 Christian Urban same as in function_common
less more (0) -1 tip