--- a/src/HOL/TPTP/TPTP_Parser/make_tptp_parser Tue Apr 03 20:42:00 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/make_tptp_parser Tue Apr 03 20:41:13 2012 +0200
@@ -30,7 +30,9 @@
for FILE in $INTERMEDIATE_FILES
do
- perl -p -e 's/\bref\b/Unsynchronized.ref/g;' -e 's/Unsafe\.(.*)/\1/g;' $FILE
+ perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \
+ -e 's/Unsafe\.(.*)/\1/g;' \
+ -e 's/\b(Char\.ord\()CharVector\.sub\b/\1String\.sub/g;' $FILE
done
) > tptp_lexyacc.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Tue Apr 03 20:42:00 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Tue Apr 03 20:41:13 2012 +0200
@@ -1342,9 +1342,9 @@
yybl := size (!yyb);
scan (s,AcceptingLeaves,l-i0,0))
end
- else let val NewChar = Char.ord(CharVector.sub(!yyb,l))
+ else let val NewChar = Char.ord(String.sub(!yyb,l))
val NewChar = if NewChar<128 then NewChar else 128
- val NewState = Char.ord(CharVector.sub(trans,NewChar))
+ val NewState = Char.ord(String.sub(trans,NewChar))
in if NewState=0 then action(l,NewAcceptingLeaves)
else scan(NewState,NewAcceptingLeaves,l+1,i0)
end