# HG changeset patch
# User wenzelm
# Date 1333478473 -7200
# Node ID 2e7e212f26d7b7f79513627cb76ae368e57dda20
# Parent  15428dd82b54d9d5fcff92f92e96803477cb0ca6# Parent  928cb8b35e6ef71ea0217fae9efeb220b6ae4660
merged

diff -r 928cb8b35e6e -r 2e7e212f26d7 src/HOL/TPTP/TPTP_Parser/make_tptp_parser
--- 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
 
diff -r 928cb8b35e6e -r 2e7e212f26d7 src/HOL/TPTP/TPTP_Parser/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