# HG changeset patch
# User wenzelm
# Date 777305633 -7200
# Node ID 756b0e2a6cac6ffc92752591cd73b37695fc3912
# Parent  01c043f610772bd09bd7a38effa152cbb995bbec
replaced Lexicon.scan_id by Scanner.scan_id;
replaced const_name by Syntax.const_name;

diff -r 01c043f61077 -r 756b0e2a6cac src/ZF/ind_syntax.ML
--- 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;