Nominal/nominal_function.ML
2012-04-30 Christian Urban adapted to change by Markus on function.ML
less more (0) -10 -1 tip