# HG changeset patch
# User nipkow
# Date 1735417233 -3600
# Node ID bac9b067c768597574a6a6941c2ff141c47826e9
# Parent  88feb0047d7c640027b43878cc02f5ca65ea3517
Backed out changeset 0ca0a47235e5 (produced Code check failed for Haskell?)

diff -r 88feb0047d7c -r bac9b067c768 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sat Dec 28 18:03:41 2024 +0100
+++ b/src/HOL/Code_Numeral.thy	Sat Dec 28 21:20:33 2024 +0100
@@ -872,26 +872,6 @@
     and (Haskell) "Prelude.abs"
     and (Scala) "_.abs"
     and (Eval) "abs"
-| constant "Bit_Operations.and :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
-    (SML) "IntInf.andb ((_),/ (_))"
-    and (OCaml) "Z.logand"
-    and (Haskell) infixl 7 ".&."
-    and (Scala) infixl 3 "&"
-| constant "Bit_Operations.or :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
-    (SML) "IntInf.orb ((_),/ (_))"
-    and (OCaml) "Z.logor"
-    and (Haskell) infixl 5 ".|."
-    and (Scala) infixl 1 "|"
-| constant "Bit_Operations.xor :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
-    (SML) "IntInf.xorb ((_),/ (_))"
-    and (OCaml) "Z.logxor"
-    and (Haskell) infixl 6 ".^."
-    and (Scala) infixl 2 "^"
-| constant "Bit_Operations.not :: integer \<Rightarrow> integer" \<rightharpoonup>
-    (SML) "IntInf.notb"
-    and (OCaml) "Z.lognot"
-    and (Haskell) "Data.Bits.complement"
-    and (Scala) "_.unary'_~"
 
 code_identifier
   code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
diff -r 88feb0047d7c -r bac9b067c768 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sat Dec 28 18:03:41 2024 +0100
+++ b/src/Tools/Code/code_haskell.ML	Sat Dec 28 21:20:33 2024 +0100
@@ -330,10 +330,6 @@
   ("Maybe", ["Nothing", "Just"])
 ];
 
-val data_bits_import_operators = [
-  ".&.", ".|.", ".^."
-];
-
 fun serialize_haskell module_prefix string_classes ctxt { module_name,
     reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program exports =
   let
@@ -383,10 +379,7 @@
       enclose "import Prelude (" ");" (commas (map str
         (map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
           @ map (fn (tyco, constrs) => (enclose (tyco ^ "(") ")" o commas o map str) constrs) prelude_import_unqualified_constr))
-      :: enclose "import Data.Bits (" ");" (commas
-        (map (str o Library.enclose "(" ")") data_bits_import_operators))
       :: print_qualified_import "Prelude"
-      :: print_qualified_import "Data.Bits"
       :: map (print_qualified_import o fst) includes;
     fun print_module module_name (gr, imports) =
       let