src/ZF/ind_syntax.ML
changeset 568 756b0e2a6cac
parent 543 e961b2092869
child 578 efc648d29dd0
     1.1 --- a/src/ZF/ind_syntax.ML	Fri Aug 19 16:12:23 1994 +0200
     1.2 +++ b/src/ZF/ind_syntax.ML	Fri Aug 19 16:13:53 1994 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4  
     1.5  (*Skipping initial blanks, find the first identifier*)
     1.6  fun scan_to_id s = 
     1.7 -    s |> explode |> take_prefix is_blank |> #2 |> Lexicon.scan_id |> #1
     1.8 +    s |> explode |> take_prefix is_blank |> #2 |> Scanner.scan_id |> #1
     1.9      handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
    1.10  
    1.11  fun is_backslash c = c = "\\";
    1.12 @@ -143,7 +143,7 @@
    1.13  	val T = (map (#2 o dest_Free) args) ---> iT
    1.14  		handle TERM _ => error 
    1.15  		    "Bad variable in constructor specification"
    1.16 -        val name = const_name id syn  (*handle infix constructors*)
    1.17 +        val name = Syntax.const_name id syn  (*handle infix constructors*)
    1.18      in ((id,T,syn), name, args, prems) end;
    1.19  
    1.20  val read_constructs = map o map o read_construct;