# HG changeset patch
# User haftmann
# Date 1737980008 -3600
# Node ID 3863850f4b0e4621bc123edadd0750cd2a7e3e36
# Parent  e23bd621eddb03cb6827ffa8d44e56385dafb9da
clarified scopes

diff -r e23bd621eddb -r 3863850f4b0e src/HOL/Library/Code_Target_Bit_Shifts.thy
--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy	Mon Jan 27 07:39:49 2025 +0100
+++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy	Mon Jan 27 13:13:28 2025 +0100
@@ -44,41 +44,31 @@
   val word_max_index : Word.word (*only for validation*)
 end = struct
 
-type int = IntInf.int;
-
-fun curry f x y = f (x, y);
+open IntInf;
 
 fun fold _ [] y = y
   | fold f (x :: xs) y = fold f xs (f x y);
 
-fun positive n = IntInf.> (n, 0);
-
-fun decr n = IntInf.- (n, 1);
-
-fun replicate n x = (if positive n then x :: replicate (decr n) x else []);
+fun replicate n x = (if n <= 0 then [] else x :: replicate (n - 1) x);
 
-val exp = curry IntInf.pow 2;
-
-val div_mod = curry IntInf.divMod;
+val max_index = pow (2, (Word.wordSize - 3)) - 1; (*experimentally determined*)
 
-val max_index = exp (Word.wordSize - 3) - 1; (*experimentally determined*)
-
-val word_of_int = Word.fromLargeInt o IntInf.toLarge;
+val word_of_int = Word.fromLargeInt o toLarge;
 
 val word_max_index = word_of_int max_index;
 
-fun words_of_int k = case div_mod k max_index
+fun words_of_int k = case divMod (k, max_index)
   of (b, s) => word_of_int s :: (replicate b word_max_index);
 
-fun push' i k = IntInf.<< (k, i);
+fun push' i k = << (k, i);
 
-fun drop' i k = IntInf.~>> (k, i);
+fun drop' i k = ~>> (k, i);
 
 (* The implementations are formally total, though indices >~ max_index will produce heavy computation load *)
 
-fun push i = fold push' (words_of_int (IntInf.abs i));
+fun push i = fold push' (words_of_int (abs i));
 
-fun drop i = fold drop' (words_of_int (IntInf.abs i));
+fun drop i = fold drop' (words_of_int (abs i));
 
 end;\<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
     and (OCaml) \<open>
@@ -87,8 +77,6 @@
   val drop : Z.t -> Z.t -> Z.t
 end = struct
 
-let curry f x y = f (x, y);;
-
 let rec fold f xs y = match xs with
   [] -> y
   | (x :: xs) -> fold f xs (f x y);;
diff -r e23bd621eddb -r 3863850f4b0e src/HOL/String.thy
--- a/src/HOL/String.thy	Mon Jan 27 07:39:49 2025 +0100
+++ b/src/HOL/String.thy	Mon Jan 27 13:13:28 2025 +0100
@@ -775,9 +775,9 @@
   then k
   else raise Fail "Non-ASCII character in literal";
 
-val char_of_ascii = Char.chr o IntInf.toInt o (fn k => k mod 128);
+val char_of_ascii = Char.chr o toInt o (fn k => k mod 128);
 
-val ascii_of_char = check_ascii o IntInf.fromInt o Char.ord;
+val ascii_of_char = check_ascii o fromInt o Char.ord;
 
 val literal_of_asciis = String.implode o map char_of_ascii;