src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML

 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000"
 ),
 (0, "")]
 fun f x = x 
-val s = map f (rev (tl (rev s))) 
+val s = List.map f (List.rev (tl (List.rev s))) 
 exception LexHackingError 
 fun look ((j,x)::r, i: int) = if i = j then x else look(r, i) 
   | look ([], i) = raise LexHackingError
 fun g {fin=x, trans=i} = {fin=x, trans=look(s,i)} 
-in Vector.fromList(map g 
+in Vector.fromList(List.map g 
 [{fin = [], trans = 0},
 {fin = [(N 2)], trans = 1},
 {fin = [(N 2)], trans = 1},
 {fin = [(N 84)], trans = 3},
 {fin = [(N 71)], trans = 0},

 	let fun action (i,nil) = raise LexError
 	| action (i,nil::l) = action (i-1,l)
 	| action (i,(node::acts)::l) =
 		case node of
 		    Internal.N yyk => 
-			(let fun yymktext() = substring(!yyb,i0,i-i0)
+			(let fun yymktext() = String.substring(!yyb,i0,i-i0)
 			     val yypos = i0+ !yygone
 			open UserDeclarations Internal.StartStates
  in (yybufpos := i; case yyk of 
 
 			(* Application actions *)

 	val NewAcceptingLeaves = fin::AcceptingLeaves
 	in if l = !yybl then
 	     if trans = #trans(Vector.sub(Internal.tab,0))
 	       then action(l,NewAcceptingLeaves
 ) else	    let val newchars= if !yydone then "" else yyinput 1024
-	    in if (size newchars)=0
+	    in if (String.size newchars)=0
 		  then (yydone := true;
 		        if (l=i0) then UserDeclarations.eof yyarg
 		                  else action(l,NewAcceptingLeaves))
 		  else (if i0=l then yyb := newchars
-		     else yyb := substring(!yyb,i0,l-i0)^newchars;
+		     else yyb := String.substring(!yyb,i0,l-i0)^newchars;
 		     yygone := !yygone+i0;
-		     yybl := size (!yyb);
+		     yybl := String.size (!yyb);
 		     scan (s,AcceptingLeaves,l-i0,0))
 	    end
 	  else let val NewChar = Char.ord(String.sub(!yyb,l))
 		val NewChar = if NewChar<128 then NewChar else 128
 		val NewState = Char.ord(String.sub(trans,NewChar))
 		in if NewState=0 then action(l,NewAcceptingLeaves)
 		else scan(NewState,NewAcceptingLeaves,l+1,i0)
 	end
 	end
 (*
-	val start= if substring(!yyb,!yybufpos-1,1)="\n"
+	val start= if String.substring(!yyb,!yybufpos-1,1)="\n"
 then !yybegin+1 else !yybegin
 *)
 	in scan(!yybegin (* start *),nil,!yybufpos,!yybufpos)
     end
 in continue end

   val memo = Array.array(numstates+numrules,ERROR)
   val _ =let fun g i=(Array.update(memo,i,REDUCE(i-numstates)); g(i+1))
        fun f i =
             if i=numstates then g i
             else (Array.update(memo,i,SHIFT (STATE i)); f (i+1))
-          in f 0 handle Subscript => ()
+          in f 0 handle General.Subscript => ()
           end
 in
 val entry_to_action = fn 0 => ACCEPT | 1 => ERROR | j => Array.sub(memo,(j-2))
 end
 val gotoT=Array.fromList(string_to_table(string_to_pairlist(NT,STATE),gotoT))
 val actionRows=string_to_table(string_to_pairlist_default(T,entry_to_action),actionRows)
 val actionRowNumbers = string_to_list actionRowNumbers
 val actionT = let val actionRowLookUp=
 let val a=Array.fromList(actionRows) in fn i=>Array.sub(a,i) end
-in Array.fromList(map actionRowLookUp actionRowNumbers)
+in Array.fromList(List.map actionRowLookUp actionRowNumbers)
 end
 in LrTable.mkLrTable {actions=actionT,gotos=gotoT,numRules=numrules,
 numStates=numstates,initialState=STATE 0}
 end
 end