src/Pure/Syntax/source.ML
Wed, 20 May 1998 18:58:13 +0200 wenzelm changed get_single: ('a, 'b) source -> 'a option * ('a, 'b) source;
less more (0) -1 tip