# HG changeset patch
# User haftmann
# Date 1737047251 -3600
# Node ID 1085eb118dc7c5c162eee5ac4a16c854e4e31953
# Parent  e31120ed89c9096c6505e9fb6bb32ed8ec4f1fb7
restrict check to PolyML

diff -r e31120ed89c9 -r 1085eb118dc7 src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy
--- a/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Thu Jan 16 10:09:42 2025 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Thu Jan 16 18:07:31 2025 +0100
@@ -60,25 +60,24 @@
 test_code check in GHC
 test_code check in Scala
 
-text \<open>Checking the index maximum for \<text>\<open>SML\<close>\<close>
+text \<open>Checking the index maximum for \<text>\<open>PolyML\<close>\<close>
+
+definition \<open>check_max = ()\<close>
 
-ML \<open>
+definition \<open>anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\<close>
+
+code_printing
+    code_module Check_Max  \<rightharpoonup>
+      (SML) \<open>
 fun check_max max =
   let
     val _ = IntInf.~>> (0, max);
-    val _ = \<^assert> ((IntInf.~>> (0, Word.+ (max, Word.fromInt 1)); false) handle Size => true)
+    val _ = ((IntInf.~>> (0, Word.+ (max, Word.fromInt 1)); raise Fail "Bad max") handle Size => ())
   in () end;
 \<close>
-
-definition \<open>check_max = ()\<close>
-
-code_printing constant check \<rightharpoonup>
-  (Eval) "check'_max Bit'_Shifts.word'_max'_index"
+  | constant check_max \<rightharpoonup>
+      (SML) "check'_max Bit'_Shifts.word'_max'_index"
 
-definition \<open>anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\<close>
-
-ML \<open>
-\<^code>\<open>anchor\<close>;
-\<close>
+test_code \<open>snd anchor = ()\<close> in PolyML
 
 end