From 5a0b95c7180c6e718de2ead2a1e8dcc142f06510 Mon Sep 17 00:00:00 2001
From: Nikolaus Huber <mail@n-huber.eu>
Date: Sat, 24 Oct 2026 17:01:09 +0100
Subject: [PATCH] include _abort as an expression

---
 Python.thy                                           |  4 ++--
 code_python.ML                                       |  7 +++++--
 test/diff/golden/Python_Examples.Example/Example.py  |  3 +++
 .../Example_class_dicts.py                           |  3 +++
 .../Python_Examples.Example_class_dicts/HOL.py       |  3 +++
 .../Python_Examples.Example_class_dicts/Int.py       |  3 +++
 .../Python_Examples.Example_class_dicts/Num.py       |  3 +++
 .../Python_Examples.Example_class_dicts/Orderings.py |  3 +++
 .../Product_Type.py                                  |  3 +++
 .../Example_classrel.py                              |  3 +++
 .../Example_classrel_base.py                         |  3 +++
 .../Example_code_numerals.py                         |  3 +++
 .../Python_Examples.Example_code_numerals/Num.py     |  3 +++
 .../Example_generic_list_pair.py                     |  3 +++
 .../List.py                                          |  3 +++
 .../Product_Type.py                                  |  3 +++
 .../Python_Examples.Example_iarray/Example_iarray.py |  3 +++
 .../golden/Python_Examples.Example_iarray/HOL.py     |  3 +++
 .../golden/Python_Examples.Example_iarray/IArray.py  |  3 +++
 .../golden/Python_Examples.Example_iarray/List.py    |  3 +++
 .../golden/Python_Examples.Example_iarray/Nat.py     |  3 +++
 .../golden/Python_Examples.Example_iarray/Num.py     |  3 +++
 .../Example_int_arith.py                             |  3 +++
 .../golden/Python_Examples.Example_int_arith/Num.py  |  3 +++
 .../Python_Examples.Example_integer_bit_ops/Arith.py |  3 +++
 .../Example_integer_bit_ops.py                       |  3 +++
 .../Groups.py                                        |  3 +++
 .../Python_Examples.Example_integer_bit_ops/Num.py   |  3 +++
 .../Python_Examples.Example_integer_bit_ops/Power.py |  3 +++
 .../Example_lambda_case.py                           |  3 +++
 .../Python_Examples.Example_lambda_case/Option.py    |  3 +++
 .../Python_Examples.Example_lists/Example_lists.py   |  3 +++
 .../diff/golden/Python_Examples.Example_lists/Num.py |  3 +++
 .../Python_Examples.Example_nat/Example_nat.py       |  3 +++
 test/diff/golden/Python_Examples.Example_nat/Num.py  |  3 +++
 .../Example_nat_edge_cases.py                        |  3 +++
 .../Python_Examples.Example_nat_edge_cases/Num.py    |  3 +++
 .../Example_nat_pattern.py                           |  3 +++
 .../Python_Examples.Example_nat_pattern/Num.py       |  3 +++
 .../Example_nested_case.py                           |  3 +++
 .../Python_Examples.Example_nested_case/Num.py       |  3 +++
 .../Example_nested_if.py                             |  3 +++
 .../golden/Python_Examples.Example_nested_if/Num.py  |  3 +++
 .../Python_Examples.Example_no_eqs/Example_no_eqs.py |  3 +++
 .../golden/Python_Examples.Example_no_eqs/HOL.py     |  3 +++
 .../Example_options.py                               |  3 +++
 .../golden/Python_Examples.Example_options/Num.py    |  3 +++
 .../golden/Python_Examples.Example_options/Option.py |  3 +++
 .../Example_partial.py                               |  3 +++
 .../golden/Python_Examples.Example_partial/Num.py    |  3 +++
 .../Example_polymorphic_const.py                     |  3 +++
 .../Python_Examples.Example_polymorphic_const/Num.py |  3 +++
 .../Example_record_ext.py                            |  3 +++
 .../golden/Python_Examples.Example_record_ext/Num.py |  3 +++
 .../Example_records.py                               |  3 +++
 .../golden/Python_Examples.Example_records/Num.py    |  3 +++
 .../Python_Examples.Example_super/Example_super.py   |  3 +++
 .../Example_super_chain.py                           |  3 +++
 .../Example_tail_calls.py                            |  3 +++
 .../loops/Example_tail_calls_loops.py                |  3 +++
 .../Example_transparent_wrapper.py                   |  3 +++
 .../Python_Examples.Example_tuples/Example_tuples.py |  3 +++
 .../golden/Python_Examples.Example_tuples/Num.py     |  3 +++
 .../Example_tyclass.py                               |  3 +++
 .../Example_unused_arg.py                            |  3 +++
 test/quick/Quick_Test.thy                            |  9 +++++++++
 test/quick/run_test.py                               | 12 ++++++++++++
 67 files changed, 217 insertions(+), 4 deletions(-)

diff --git a/Python.thy b/Python.thy
index 278b140..ead5b8f 100644
--- a/Python.thy
+++ b/Python.thy
@@ -9,9 +9,9 @@ declare [[default_code_width = 2000]]
 code_identifier
   code_module Code_Numeral \<rightharpoonup> (Python) Arith
 
-(* Panic *)
+(* Panic, by a helper function, since Code.abort occurs in expression position *)
 code_printing
-  constant Code.abort \<rightharpoonup> (Python) "raise RuntimeError(\"_\")"
+  constant Code.abort \<rightharpoonup> (Python) "'_abort"
 
 (* unit *)
 code_printing
diff --git a/code_python.ML b/code_python.ML
index de72bae..929b9fc 100644
--- a/code_python.ML
+++ b/code_python.ML
@@ -74,7 +74,7 @@ val python_reserved_words =
    "raise", "return", "try", "while", "with", "yield", "match", "case"]
 
   (* these are symbols we use in addition to the standard reserved words *) 
-  @ ["dataclass", "Any", "Callable", "_unimplemented", "functools"];;
+  @ ["dataclass", "Any", "Callable", "_unimplemented", "_abort", "functools"];;
 
 type eqtn = { 
   patterns: iterm list,       (* left hand side pattern list *)
@@ -1067,7 +1067,10 @@ fun serialize_python undefineds _ ctxt { module_name, reserved_syms,
         val unimplemented_def = Pretty.chunks
           [Pretty.str "def _unimplemented(name):",
            indent_block 4 (Pretty.str "raise NotImplementedError(name)")]
-      in ([mod_name ^ ".py"], Pretty.chunks2 (imports_block :: unimplemented_def :: stmt_ps))
+        val abort_def = Pretty.chunks
+          [Pretty.str "def _abort(msg, thunk):",
+           indent_block 4 (Pretty.str "raise RuntimeError(msg)")]
+      in ([mod_name ^ ".py"], Pretty.chunks2 (imports_block :: unimplemented_def :: abort_def :: stmt_ps))
       end;
 
     val p = map print_one_module module_stmts
diff --git a/test/diff/golden/Python_Examples.Example/Example.py b/test/diff/golden/Python_Examples.Example/Example.py
index 2bbabeb..70eb3a6 100644
--- a/test/diff/golden/Python_Examples.Example/Example.py
+++ b/test/diff/golden/Python_Examples.Example/Example.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class Red:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Example_class_dicts.py b/test/diff/golden/Python_Examples.Example_class_dicts/Example_class_dicts.py
index 83c83ec..78fe428 100644
--- a/test/diff/golden/Python_Examples.Example_class_dicts/Example_class_dicts.py
+++ b/test/diff/golden/Python_Examples.Example_class_dicts/Example_class_dicts.py
@@ -9,6 +9,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def weight(a_dict, x, xa1):
     match (x, xa1):
         case (xa, []):
diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py b/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py
index 0134fe9..ff381e0 100644
--- a/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py
+++ b/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class equal:
     equala: Callable
diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Int.py b/test/diff/golden/Python_Examples.Example_class_dicts/Int.py
index d828248..77953db 100644
--- a/test/diff/golden/Python_Examples.Example_class_dicts/Int.py
+++ b/test/diff/golden/Python_Examples.Example_class_dicts/Int.py
@@ -7,6 +7,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @functools.cache
 def equal_int():
     return HOL.equal(equala = lambda a, b: (a == b))
diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Num.py b/test/diff/golden/Python_Examples.Example_class_dicts/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_class_dicts/Num.py
+++ b/test/diff/golden/Python_Examples.Example_class_dicts/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py b/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py
index 3ec0149..bf86827 100644
--- a/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py
+++ b/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class ord:
     less_eq: Callable
diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py b/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py
index 8e3911a..816caa6 100644
--- a/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py
+++ b/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def equal_proda(a_dict, b_dict, x0, x1):
     match (x0, x1):
         case ((x1a, x2), (y1, y2)):
diff --git a/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py
index 02d9206..c6c9396 100644
--- a/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py
+++ b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py
@@ -6,6 +6,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def sup_apply_bool(b):
     return (b)
 
diff --git a/test/diff/golden/Python_Examples.Example_classrel/Example_classrel_base.py b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel_base.py
index 8d4bdb7..5a70b24 100644
--- a/test/diff/golden/Python_Examples.Example_classrel/Example_classrel_base.py
+++ b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel_base.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class super_op:
     sup_apply: Callable
diff --git a/test/diff/golden/Python_Examples.Example_code_numerals/Example_code_numerals.py b/test/diff/golden/Python_Examples.Example_code_numerals/Example_code_numerals.py
index 8ab5c8f..b912cab 100644
--- a/test/diff/golden/Python_Examples.Example_code_numerals/Example_code_numerals.py
+++ b/test/diff/golden/Python_Examples.Example_code_numerals/Example_code_numerals.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def cn_add(x, y):
     return ((x + y))
 
diff --git a/test/diff/golden/Python_Examples.Example_code_numerals/Num.py b/test/diff/golden/Python_Examples.Example_code_numerals/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_code_numerals/Num.py
+++ b/test/diff/golden/Python_Examples.Example_code_numerals/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_generic_list_pair/Example_generic_list_pair.py b/test/diff/golden/Python_Examples.Example_generic_list_pair/Example_generic_list_pair.py
index 03938a0..f3e0e53 100644
--- a/test/diff/golden/Python_Examples.Example_generic_list_pair/Example_generic_list_pair.py
+++ b/test/diff/golden/Python_Examples.Example_generic_list_pair/Example_generic_list_pair.py
@@ -6,6 +6,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def swap(x0):
     match x0:
         case Product_Type.Pair(x, y):
diff --git a/test/diff/golden/Python_Examples.Example_generic_list_pair/List.py b/test/diff/golden/Python_Examples.Example_generic_list_pair/List.py
index 61b9c7b..5935c4c 100644
--- a/test/diff/golden/Python_Examples.Example_generic_list_pair/List.py
+++ b/test/diff/golden/Python_Examples.Example_generic_list_pair/List.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class Nil:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_generic_list_pair/Product_Type.py b/test/diff/golden/Python_Examples.Example_generic_list_pair/Product_Type.py
index 9d91185..4477e75 100644
--- a/test/diff/golden/Python_Examples.Example_generic_list_pair/Product_Type.py
+++ b/test/diff/golden/Python_Examples.Example_generic_list_pair/Product_Type.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class Pair:
     a: Any
diff --git a/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py b/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py
index b35bb0d..f99cf74 100644
--- a/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py
+++ b/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py
@@ -7,6 +7,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def sum_ends(a):
     return (((a[0]) + (a[(max(0, (len(a)) - 1))])))
 
diff --git a/test/diff/golden/Python_Examples.Example_iarray/HOL.py b/test/diff/golden/Python_Examples.Example_iarray/HOL.py
index 0134fe9..ff381e0 100644
--- a/test/diff/golden/Python_Examples.Example_iarray/HOL.py
+++ b/test/diff/golden/Python_Examples.Example_iarray/HOL.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class equal:
     equala: Callable
diff --git a/test/diff/golden/Python_Examples.Example_iarray/IArray.py b/test/diff/golden/Python_Examples.Example_iarray/IArray.py
index 4403b0e..a5d0f38 100644
--- a/test/diff/golden/Python_Examples.Example_iarray/IArray.py
+++ b/test/diff/golden/Python_Examples.Example_iarray/IArray.py
@@ -6,5 +6,8 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def equal_iarray(a_dict, asa, bs):
     return (List.equal_list(a_dict, (list(asa)), (list(bs))))
diff --git a/test/diff/golden/Python_Examples.Example_iarray/List.py b/test/diff/golden/Python_Examples.Example_iarray/List.py
index 7b82d6e..1aad452 100644
--- a/test/diff/golden/Python_Examples.Example_iarray/List.py
+++ b/test/diff/golden/Python_Examples.Example_iarray/List.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def equal_list(a_dict, x0, x1):
     match (x0, x1):
         case ([], [x21, *x22]):
diff --git a/test/diff/golden/Python_Examples.Example_iarray/Nat.py b/test/diff/golden/Python_Examples.Example_iarray/Nat.py
index 04009cc..c0a5572 100644
--- a/test/diff/golden/Python_Examples.Example_iarray/Nat.py
+++ b/test/diff/golden/Python_Examples.Example_iarray/Nat.py
@@ -6,6 +6,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @functools.cache
 def equal_nat():
     return HOL.equal(equala = lambda a, b: (a == b))
diff --git a/test/diff/golden/Python_Examples.Example_iarray/Num.py b/test/diff/golden/Python_Examples.Example_iarray/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_iarray/Num.py
+++ b/test/diff/golden/Python_Examples.Example_iarray/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_int_arith/Example_int_arith.py b/test/diff/golden/Python_Examples.Example_int_arith/Example_int_arith.py
index 14f06f6..9751940 100644
--- a/test/diff/golden/Python_Examples.Example_int_arith/Example_int_arith.py
+++ b/test/diff/golden/Python_Examples.Example_int_arith/Example_int_arith.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 product = ((6 * 7))
 
 def checksum(x, y):
diff --git a/test/diff/golden/Python_Examples.Example_int_arith/Num.py b/test/diff/golden/Python_Examples.Example_int_arith/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_int_arith/Num.py
+++ b/test/diff/golden/Python_Examples.Example_int_arith/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py
index 475f11a..68365d3 100644
--- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py
+++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py
@@ -8,6 +8,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @functools.cache
 def one_integer():
     return Groups.one(onea = lambda : 1)
diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py
index 666f41f..8ce682f 100644
--- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py
+++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py
@@ -6,6 +6,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 test_bit = (Arith.bit_integer(10, 1))
 
 test_sgn = (Arith.sgn_integer(-42))
diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py
index 1172389..1553aac 100644
--- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py
+++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class one:
     onea: Callable
diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Num.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Num.py
+++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py
index 9da25a7..152fd2d 100644
--- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py
+++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class power:
     one_power: Any
diff --git a/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py b/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py
index e213bf6..6e6f61b 100644
--- a/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py
+++ b/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def doubled(xs):
     return (list(map(lambda n: (n + n), xs)))
 
diff --git a/test/diff/golden/Python_Examples.Example_lambda_case/Option.py b/test/diff/golden/Python_Examples.Example_lambda_case/Option.py
index e4fcff2..645d8a0 100644
--- a/test/diff/golden/Python_Examples.Example_lambda_case/Option.py
+++ b/test/diff/golden/Python_Examples.Example_lambda_case/Option.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class Nonea:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_lists/Example_lists.py b/test/diff/golden/Python_Examples.Example_lists/Example_lists.py
index 1f08ca9..77a01ad 100644
--- a/test/diff/golden/Python_Examples.Example_lists/Example_lists.py
+++ b/test/diff/golden/Python_Examples.Example_lists/Example_lists.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 example = ([1, 2, 3])
 
 def prepend(x, xs):
diff --git a/test/diff/golden/Python_Examples.Example_lists/Num.py b/test/diff/golden/Python_Examples.Example_lists/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_lists/Num.py
+++ b/test/diff/golden/Python_Examples.Example_lists/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_nat/Example_nat.py b/test/diff/golden/Python_Examples.Example_nat/Example_nat.py
index caefc81..74b6da9 100644
--- a/test/diff/golden/Python_Examples.Example_nat/Example_nat.py
+++ b/test/diff/golden/Python_Examples.Example_nat/Example_nat.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 nat_sum = ((6 + 7))
 
 nat_eq_test = ((4 == 4))
diff --git a/test/diff/golden/Python_Examples.Example_nat/Num.py b/test/diff/golden/Python_Examples.Example_nat/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_nat/Num.py
+++ b/test/diff/golden/Python_Examples.Example_nat/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_nat_edge_cases/Example_nat_edge_cases.py b/test/diff/golden/Python_Examples.Example_nat_edge_cases/Example_nat_edge_cases.py
index 494a942..dd06d07 100644
--- a/test/diff/golden/Python_Examples.Example_nat_edge_cases/Example_nat_edge_cases.py
+++ b/test/diff/golden/Python_Examples.Example_nat_edge_cases/Example_nat_edge_cases.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def peel_positive_head(x0):
     match x0:
         case []:
diff --git a/test/diff/golden/Python_Examples.Example_nat_edge_cases/Num.py b/test/diff/golden/Python_Examples.Example_nat_edge_cases/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_nat_edge_cases/Num.py
+++ b/test/diff/golden/Python_Examples.Example_nat_edge_cases/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_nat_pattern/Example_nat_pattern.py b/test/diff/golden/Python_Examples.Example_nat_pattern/Example_nat_pattern.py
index 2f9657a..934f9ad 100644
--- a/test/diff/golden/Python_Examples.Example_nat_pattern/Example_nat_pattern.py
+++ b/test/diff/golden/Python_Examples.Example_nat_pattern/Example_nat_pattern.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def fact(n):
     if ((n == 0)):
         return (1)
diff --git a/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py b/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py
+++ b/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_nested_case/Example_nested_case.py b/test/diff/golden/Python_Examples.Example_nested_case/Example_nested_case.py
index 83c2d13..5e966dd 100644
--- a/test/diff/golden/Python_Examples.Example_nested_case/Example_nested_case.py
+++ b/test/diff/golden/Python_Examples.Example_nested_case/Example_nested_case.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def weird(n):
     if ((n == 0)):
         return (1)
diff --git a/test/diff/golden/Python_Examples.Example_nested_case/Num.py b/test/diff/golden/Python_Examples.Example_nested_case/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_nested_case/Num.py
+++ b/test/diff/golden/Python_Examples.Example_nested_case/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_nested_if/Example_nested_if.py b/test/diff/golden/Python_Examples.Example_nested_if/Example_nested_if.py
index cbc70de..c273e55 100644
--- a/test/diff/golden/Python_Examples.Example_nested_if/Example_nested_if.py
+++ b/test/diff/golden/Python_Examples.Example_nested_if/Example_nested_if.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def grade_code(score):
     if ((score < 60)):
         return (0)
diff --git a/test/diff/golden/Python_Examples.Example_nested_if/Num.py b/test/diff/golden/Python_Examples.Example_nested_if/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_nested_if/Num.py
+++ b/test/diff/golden/Python_Examples.Example_nested_if/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py b/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py
index bdb77e2..b6e32a6 100644
--- a/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py
+++ b/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py
@@ -5,4 +5,7 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 uses_undefined = (HOL.undefined())
diff --git a/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py b/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py
index bf23ee4..dab8256 100644
--- a/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py
+++ b/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py
@@ -4,5 +4,8 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def undefined():
     raise NotImplementedError("HOL.undefined")
diff --git a/test/diff/golden/Python_Examples.Example_options/Example_options.py b/test/diff/golden/Python_Examples.Example_options/Example_options.py
index be05357..3478ecb 100644
--- a/test/diff/golden/Python_Examples.Example_options/Example_options.py
+++ b/test/diff/golden/Python_Examples.Example_options/Example_options.py
@@ -6,6 +6,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def describe_opt(x0):
     match x0:
         case Option.Nonea():
diff --git a/test/diff/golden/Python_Examples.Example_options/Num.py b/test/diff/golden/Python_Examples.Example_options/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_options/Num.py
+++ b/test/diff/golden/Python_Examples.Example_options/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_options/Option.py b/test/diff/golden/Python_Examples.Example_options/Option.py
index e4fcff2..645d8a0 100644
--- a/test/diff/golden/Python_Examples.Example_options/Option.py
+++ b/test/diff/golden/Python_Examples.Example_options/Option.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class Nonea:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_partial/Example_partial.py b/test/diff/golden/Python_Examples.Example_partial/Example_partial.py
index 8fa829e..62419c5 100644
--- a/test/diff/golden/Python_Examples.Example_partial/Example_partial.py
+++ b/test/diff/golden/Python_Examples.Example_partial/Example_partial.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def add2(x, y):
     return ((x + y))
 
diff --git a/test/diff/golden/Python_Examples.Example_partial/Num.py b/test/diff/golden/Python_Examples.Example_partial/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_partial/Num.py
+++ b/test/diff/golden/Python_Examples.Example_partial/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_polymorphic_const/Example_polymorphic_const.py b/test/diff/golden/Python_Examples.Example_polymorphic_const/Example_polymorphic_const.py
index 0409c7c..4993801 100644
--- a/test/diff/golden/Python_Examples.Example_polymorphic_const/Example_polymorphic_const.py
+++ b/test/diff/golden/Python_Examples.Example_polymorphic_const/Example_polymorphic_const.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 empty_list = ([])
 
 magic_number = (42)
diff --git a/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py b/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py
+++ b/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py b/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py
index 722a393..013f722 100644
--- a/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py
+++ b/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class point_exta:
     px: Any
diff --git a/test/diff/golden/Python_Examples.Example_record_ext/Num.py b/test/diff/golden/Python_Examples.Example_record_ext/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_record_ext/Num.py
+++ b/test/diff/golden/Python_Examples.Example_record_ext/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_records/Example_records.py b/test/diff/golden/Python_Examples.Example_records/Example_records.py
index 7001c66..991ce03 100644
--- a/test/diff/golden/Python_Examples.Example_records/Example_records.py
+++ b/test/diff/golden/Python_Examples.Example_records/Example_records.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class point_exta:
     px: Any
diff --git a/test/diff/golden/Python_Examples.Example_records/Num.py b/test/diff/golden/Python_Examples.Example_records/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_records/Num.py
+++ b/test/diff/golden/Python_Examples.Example_records/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_super/Example_super.py b/test/diff/golden/Python_Examples.Example_super/Example_super.py
index 6a3501d..ab75e78 100644
--- a/test/diff/golden/Python_Examples.Example_super/Example_super.py
+++ b/test/diff/golden/Python_Examples.Example_super/Example_super.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class Red:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_super_chain/Example_super_chain.py b/test/diff/golden/Python_Examples.Example_super_chain/Example_super_chain.py
index a26386f..9a97453 100644
--- a/test/diff/golden/Python_Examples.Example_super_chain/Example_super_chain.py
+++ b/test/diff/golden/Python_Examples.Example_super_chain/Example_super_chain.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class Box:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py b/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py
index ed0efe7..105517f 100644
--- a/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py
+++ b/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class ord:
     less_eq: Callable
diff --git a/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py b/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py
index 1cd3db1..a97206b 100644
--- a/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py
+++ b/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class ord:
     less_eq: Callable
diff --git a/test/diff/golden/Python_Examples.Example_transparent_wrapper/Example_transparent_wrapper.py b/test/diff/golden/Python_Examples.Example_transparent_wrapper/Example_transparent_wrapper.py
index 254cc68..897a90b 100644
--- a/test/diff/golden/Python_Examples.Example_transparent_wrapper/Example_transparent_wrapper.py
+++ b/test/diff/golden/Python_Examples.Example_transparent_wrapper/Example_transparent_wrapper.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def unbox(n):
     return (n)
 
diff --git a/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py b/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py
index 5d3e48f..a6d17bc 100644
--- a/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py
+++ b/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 point = ((3, 4))
 
 triple = ((1, ((2, 3))))
diff --git a/test/diff/golden/Python_Examples.Example_tuples/Num.py b/test/diff/golden/Python_Examples.Example_tuples/Num.py
index fc191a7..c4907ac 100644
--- a/test/diff/golden/Python_Examples.Example_tuples/Num.py
+++ b/test/diff/golden/Python_Examples.Example_tuples/Num.py
@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py b/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py
index 748b17e..0868ed6 100644
--- a/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py
+++ b/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py
@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class Red:
     pass
diff --git a/test/diff/golden/Python_Examples.Example_unused_arg/Example_unused_arg.py b/test/diff/golden/Python_Examples.Example_unused_arg/Example_unused_arg.py
index 9a55018..63451dd 100644
--- a/test/diff/golden/Python_Examples.Example_unused_arg/Example_unused_arg.py
+++ b/test/diff/golden/Python_Examples.Example_unused_arg/Example_unused_arg.py
@@ -4,5 +4,8 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def const_fn(x, uu, uv):
     return ((x + 1))
diff --git a/test/quick/Quick_Test.thy b/test/quick/Quick_Test.thy
index b9a8d20..841eb56 100644
--- a/test/quick/Quick_Test.thy
+++ b/test/quick/Quick_Test.thy
@@ -264,7 +264,16 @@ definition twice_twice :: "'a::plus \<Rightarrow> 'a" where
   "twice_twice = (\<lambda>x. x + x) \<circ> (\<lambda>x. x + x)"
 definition e_twice_twice :: int where "e_twice_twice = twice_twice 3"
 
+section \<open>Code.abort in expression position\<close>
+
+definition a_checked :: "int \<Rightarrow> int" where
+  "a_checked x = (if x < 0 then Code.abort (STR ''negative'') (\<lambda>_. x) else x)"
+
+definition a_nested :: "int \<Rightarrow> int" where
+  "a_nested x = 1 + (if x < 0 then Code.abort (STR ''negative'') (\<lambda>_. x) else x)"
+
 export_code
+  a_checked a_nested
   t_point t_swap t_add_points t_points_sum
   i_quotient_neg i_remainder_neg i_checksum
   n_sub_trunc n_sub_pos n_literal
diff --git a/test/quick/run_test.py b/test/quick/run_test.py
index 7feb210..8cddd9b 100644
--- a/test/quick/run_test.py
+++ b/test/quick/run_test.py
@@ -40,6 +40,18 @@ def _find_example_all():
     import Quick_Test as m
 
 
+# ---- Code.abort ----
+
+
+def test_abort_in_expression():
+    assert m.a_checked(3) == 3
+    assert m.a_nested(3) == 4
+    with pytest.raises(RuntimeError, match="negative"):
+        m.a_checked(-1)
+    with pytest.raises(RuntimeError, match="negative"):
+        m.a_nested(-1)
+
+
 # ---- tuples ----
 
 def test_tuple_values():