# HG changeset patch
# User blanchet
# Date 1407246939 -7200
# Node ID 7d319d6ccde09541845aa65587b0a1e94a0dceda
# Parent  07521fed607134eab8ef6f71a9a0d0bbbc543aec
regenerated ML-Lex/Yacc files

diff -r 07521fed6071 -r 7d319d6ccde0 src/HOL/TPTP/TPTP_Parser/README
--- a/src/HOL/TPTP/TPTP_Parser/README	Tue Aug 05 15:54:47 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/README	Tue Aug 05 15:55:39 2014 +0200
@@ -29,4 +29,4 @@
 ML-Yacc's library.
 
 Nik Sultana
-9th March 2012
\ No newline at end of file
+9th March 2012
diff -r 07521fed6071 -r 7d319d6ccde0 src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML	Tue Aug 05 15:54:47 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML	Tue Aug 05 15:55:39 2014 +0200
@@ -1143,12 +1143,12 @@
 ),
 (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},
@@ -1328,7 +1328,7 @@
 	| 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 
@@ -1414,14 +1414,14 @@
 	     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))
@@ -1432,7 +1432,7 @@
 	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)
@@ -3604,7 +3604,7 @@
        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))
@@ -3614,7 +3614,7 @@
 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}