diff --git a/experiments/2026-05-12-cross-model-authoring/master/spec.md b/experiments/2026-05-12-cross-model-authoring/master/spec.md
index 93e7913..7e78ac4 100644
--- a/experiments/2026-05-12-cross-model-authoring/master/spec.md
+++ b/experiments/2026-05-12-cross-model-authoring/master/spec.md
@@ -303,11 +303,14 @@ constructors have an empty argument list.
 Example: `(data List (ctor Nil) (ctor Cons Int (con List)))` is a
 monomorphic Int list with a Nil and a Cons constructor.
 
-Constructor invocation: `(ctor TYPE-NAME CTOR-NAME ARG*)`. The
-`TYPE-NAME` precedes the constructor name so the parser does not
-need a separate registry to resolve overlapping constructor names
-across ADTs. Example: `(ctor List Cons 1 (ctor List Nil))` builds a
-single-element list.
+Constructor invocation: `(term-ctor TYPE-NAME CTOR-NAME ARG*)`.
+The Form-A keyword is `term-ctor`, not `ctor` — the bare `(ctor
+...)` is reserved for the inside of `(data ...)` definitions and
+the parser rejects it in term position. `TYPE-NAME` precedes the
+constructor name so the parser does not need a separate registry
+to resolve overlapping constructor names across ADTs. Example:
+`(term-ctor List Cons 1 (term-ctor List Nil))` builds a single-
+element list.
 {/form-only}
 
 {example: data_simple}
@@ -359,7 +362,8 @@ Pattern shapes:
 - Variable: a bare identifier alone, e.g. `h`, binds the scrutinee.
 - Literal: a literal value alone, e.g. `0`, `true`, `"abc"`,
   `(unit)`, matches bit-equal scrutinees.
-- Constructor: `(ctor CTOR-NAME SUBPAT*)` — note no `type` slot
+- Constructor: `(pat-ctor CTOR-NAME SUBPAT*)` — the Form-A
+  pattern keyword is `pat-ctor` (not `ctor`). No `type` slot
   here, because the constructor name is resolved against the
   scrutinee's type.
 
diff --git a/experiments/2026-05-12-cross-model-authoring/rendered/ail.md b/experiments/2026-05-12-cross-model-authoring/rendered/ail.md
index 2efd433..dae036e 100644
--- a/experiments/2026-05-12-cross-model-authoring/rendered/ail.md
+++ b/experiments/2026-05-12-cross-model-authoring/rendered/ail.md
@@ -252,11 +252,14 @@ constructors have an empty argument list.
 Example: `(data List (ctor Nil) (ctor Cons Int (con List)))` is a
 monomorphic Int list with a Nil and a Cons constructor.
 
-Constructor invocation: `(ctor TYPE-NAME CTOR-NAME ARG*)`. The
-`TYPE-NAME` precedes the constructor name so the parser does not
-need a separate registry to resolve overlapping constructor names
-across ADTs. Example: `(ctor List Cons 1 (ctor List Nil))` builds a
-single-element list.
+Constructor invocation: `(term-ctor TYPE-NAME CTOR-NAME ARG*)`.
+The Form-A keyword is `term-ctor`, not `ctor` — the bare `(ctor
+...)` is reserved for the inside of `(data ...)` definitions and
+the parser rejects it in term position. `TYPE-NAME` precedes the
+constructor name so the parser does not need a separate registry
+to resolve overlapping constructor names across ADTs. Example:
+`(term-ctor List Cons 1 (term-ctor List Nil))` builds a single-
+element list.
 
 ```ail
 (module data_simple
@@ -299,7 +302,8 @@ Pattern shapes:
 - Variable: a bare identifier alone, e.g. `h`, binds the scrutinee.
 - Literal: a literal value alone, e.g. `0`, `true`, `"abc"`,
   `(unit)`, matches bit-equal scrutinees.
-- Constructor: `(ctor CTOR-NAME SUBPAT*)` — note no `type` slot
+- Constructor: `(pat-ctor CTOR-NAME SUBPAT*)` — the Form-A
+  pattern keyword is `pat-ctor` (not `ctor`). No `type` slot
   here, because the constructor name is resolved against the
   scrutinee's type.
 
@@ -349,13 +353,13 @@ arms or into code outside the `match`.
 
 Every function type carries an effect row — a set of effect labels
 that the function may raise. The two currently wired effects are
-`IO` (required to call effect operations like `io/print_str`) and
+`IO` (required to call effect operations like `io/print_int`) and
 `Diverge` (used for functions that may not terminate). An empty
 effect row marks the function as pure.
 
 Effect operations are reached through the `do` term, not through a
 regular function application. The `do` form names the operation
-(e.g. `io/print_str`) and lists the operation's arguments; the
+(e.g. `io/print_int`) and lists the operation's arguments; the
 typechecker resolves the operation against the prelude's effect-op
 table, checks the arguments, and accumulates the operation's
 effect label into the enclosing function's effect row.
@@ -374,9 +378,8 @@ in canonical output.
 
 Effect operation: `(do OP-NAME ARG*)` — the leading `do` head is
 the parser's signal that the next identifier is an effect op, not a
-function. Example: `(do io/print_str "hi\n")` prints the string
-`hi` followed by a newline and raises the `IO` effect. To print a
-non-string value, first convert it: `(do io/print_str (app int_to_str 42))`.
+function. Example: `(do io/print_int 42)` prints the integer 42
+and raises the `IO` effect.
 
 Sequencing: `(seq LHS RHS)`. The value of `(seq X Y)` is `Y`'s
 value; `X`'s value is discarded. Chains of sequencing are written
@@ -386,10 +389,10 @@ value.
 ```ail
 (module fn_with_do_seq
   (fn main
-    (doc "Print two Ints in sequence. Exercises TermDo, TermSeq, the IO effect on a fn type, and int-to-str conversion via the prelude `int_to_str`. The trailing unit return is implicit in the last Do (op returns Unit).")
+    (doc "Print two Ints in sequence. Exercises TermDo, TermSeq, and the IO effect on a fn type. The trailing unit return is implicit in the last Do (op returns Unit).")
     (type (fn-type (params) (ret (con Unit)) (effects IO)))
     (params)
-    (body (seq (do io/print_str (app int_to_str 1)) (do io/print_str (app int_to_str 2))))))
+    (body (seq (do io/print_int 1) (do io/print_int 2)))))
 ```
 
 ## 9. Literals
@@ -548,14 +551,14 @@ Effect operations (reached through `do`, not `app`):
 
 | Op | Signature | Effect |
 |----|----------|-------|
+| `io/print_int` | `(Int) -> Unit` | `IO` |
+| `io/print_bool` | `(Bool) -> Unit` | `IO` |
 | `io/print_str` | `(Str) -> Unit` | `IO` |
+| `io/print_float` | `(Float) -> Unit` | `IO` |
 
-`io/print_str` is the only print operation, and it appends a
-trailing newline (the runtime calls C `puts`). To print a non-string
-value, convert it first via `int_to_str`, `float_to_str`, or
-`bool_to_str` — all three are in the prelude (see the prelude
-table above). To print two values on consecutive lines, sequence
-two `(do io/print_str ...)` calls with `seq`.
+`int_to_str` is intentionally NOT in the prelude — it is type-
+installed in a future milestone but codegen-deferred pending the
+heap-Str ABI work. Do not call it.
 
 ## 12. Content addressing