replaced Lexicon.scan_id by Scanner.scan_id;
replaced const_name by Syntax.const_name;

--- a/src/ZF/ind_syntax.ML	Fri Aug 19 16:12:23 1994 +0200
+++ b/src/ZF/ind_syntax.ML	Fri Aug 19 16:13:53 1994 +0200
@@ -71,7 +71,7 @@
 
 (*Skipping initial blanks, find the first identifier*)
 fun scan_to_id s = 
-    s |> explode |> take_prefix is_blank |> #2 |> Lexicon.scan_id |> #1
+    s |> explode |> take_prefix is_blank |> #2 |> Scanner.scan_id |> #1
     handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
 
 fun is_backslash c = c = "\\";
@@ -143,7 +143,7 @@
 	val T = (map (#2 o dest_Free) args) ---> iT
 		handle TERM _ => error 
 		    "Bad variable in constructor specification"
-        val name = const_name id syn  (*handle infix constructors*)
+        val name = Syntax.const_name id syn  (*handle infix constructors*)
     in ((id,T,syn), name, args, prems) end;
 
 val read_constructs = map o map o read_construct;