src/Pure/Isar/outer_parse.ML
changeset 28941 128459bd72d2
parent 28302 ef86de9c98aa
child 28965 1de908189869
--- a/src/Pure/Isar/outer_parse.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -228,7 +228,7 @@
 (* names and text *)
 
 val name = group "name declaration" (short_ident || sym_ident || string || number);
-val binding = position name >> Name.binding_pos;
+val binding = position name >> Binding.binding_pos;
 val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
 val path = group "file name/path specification" name >> Path.explode;