--- 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}