# HG changeset patch
# User haftmann
# Date 1190299052 -7200
# Node ID 8f94b16783f70d35db149a877552bb94b090d0bf
# Parent  6b7ac2a43df81c40bee59863c82927599b6272cf
restored ml system independence

diff -r 6b7ac2a43df8 -r 8f94b16783f7 src/HOL/Library/Pretty_Char_chr.thy
--- a/src/HOL/Library/Pretty_Char_chr.thy	Thu Sep 20 16:37:31 2007 +0200
+++ b/src/HOL/Library/Pretty_Char_chr.thy	Thu Sep 20 16:37:32 2007 +0200
@@ -38,7 +38,7 @@
   by (cases c) auto
 
 code_const int_of_char and char_of_int
-  (SML "!Char.ord" and "!Char.chr")
+  (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
   (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
   (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
 
diff -r 6b7ac2a43df8 -r 8f94b16783f7 src/HOL/Library/Pretty_Int.thy
--- a/src/HOL/Library/Pretty_Int.thy	Thu Sep 20 16:37:31 2007 +0200
+++ b/src/HOL/Library/Pretty_Int.thy	Thu Sep 20 16:37:32 2007 +0200
@@ -16,7 +16,7 @@
 *}
 
 code_type int
-  (SML "int")
+  (SML "IntInf.int")
   (OCaml "Big'_int.big'_int")
   (Haskell "Integer")
 
@@ -44,51 +44,51 @@
      and "error/ \"Bit\"")
 
 code_const Numeral.pred
-  (SML "Int.- ((_), 1)")
+  (SML "IntInf.- ((_), 1)")
   (OCaml "Big'_int.pred'_big'_int")
   (Haskell "!(_/ -/ 1)")
 
 code_const Numeral.succ
-  (SML "Int.+ ((_), 1)")
+  (SML "IntInf.+ ((_), 1)")
   (OCaml "Big'_int.succ'_big'_int")
   (Haskell "!(_/ +/ 1)")
 
 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-  (SML "Int.+ ((_), (_))")
+  (SML "IntInf.+ ((_), (_))")
   (OCaml "Big'_int.add'_big'_int")
   (Haskell infixl 6 "+")
 
 code_const "uminus \<Colon> int \<Rightarrow> int"
-  (SML "Int.~")
+  (SML "IntInf.~")
   (OCaml "Big'_int.minus'_big'_int")
   (Haskell "negate")
 
 code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-  (SML "Int.- ((_), (_))")
+  (SML "IntInf.- ((_), (_))")
   (OCaml "Big'_int.sub'_big'_int")
   (Haskell infixl 6 "-")
 
 code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-  (SML "Int.* ((_), (_))")
+  (SML "IntInf.* ((_), (_))")
   (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
 
 code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "!((_ : Int.int) = _)")
+  (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")
 
 code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "Int.<= ((_), (_))")
+  (SML "IntInf.<= ((_), (_))")
   (OCaml "Big'_int.le'_big'_int")
   (Haskell infix 4 "<=")
 
 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "Int.< ((_), (_))")
+  (SML "IntInf.< ((_), (_))")
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
 
-code_reserved SML Int
+code_reserved SML IntInf
 code_reserved OCaml Big_int
 
 end
\ No newline at end of file