diff --git a/help/Docfiles/Globals.max_print_length.doc b/help/Docfiles/Globals.max_print_length.doc
new file mode 100644
index 0000000000..4e2240010e
--- /dev/null
+++ b/help/Docfiles/Globals.max_print_length.doc
@@ -0,0 +1,22 @@
+\DOC max_print_length
+
+\TYPE {max_print_length : int ref}
+
+\SYNOPSIS
+Sets a length bound on pretty printing for list forms.
+
+\DESCRIBE
+
+Defines the maximum number of elements that the pretty printer will print for
+list forms. This closely mirrors {Globals.max_print_depth}: remaining elements
+are abbreviated by {...}, and the default value of {~1} means `print all
+elements'.
+
+\FAILURE
+Never fails.
+
+\SEEALSO
+Globals.max_print_depth
+
+
+\ENDDOC
diff --git a/src/monad/monadsyntax.sig b/src/monad/monadsyntax.sig
index 0f937390e9..4112c14b96 100644
--- a/src/monad/monadsyntax.sig
+++ b/src/monad/monadsyntax.sig
@@ -20,7 +20,6 @@ sig
   val temp_disable_monadsyntax : unit -> unit
 
   val print_explicit_monadic_lets : bool -> unit
-  val set_monad_print_length : int option -> unit
 
   type monadinfo =
        { bind : term,
diff --git a/src/monad/monadsyntax.sml b/src/monad/monadsyntax.sml
index 20f785b021..e7058da4bf 100644
--- a/src/monad/monadsyntax.sml
+++ b/src/monad/monadsyntax.sml
@@ -273,7 +273,6 @@ end handle HOL_ERR _ => NONE
 
 
 val explicit_mlets = ref false;
-val monad_print_length = ref (~1);
 
 fun print_monads (tyg, tmg) backend sysprinter ppfns (p,l,r) depth t = let
   open term_pp_types term_grammar smpp term_pp_utils
@@ -349,7 +348,8 @@ in
   ublock PP.CONSISTENT 0
     (strn "do" >> brk(1,2) >>
      getbvs >- (fn oldbvs =>
-     concatWith (strn ";" >> brk(1,2)) (pr_action_list (!monad_print_length) actions) >>
+     concatWith (strn ";" >> brk(1,2))
+      (pr_action_list (!Globals.max_print_length) actions) >>
      brk(1,0) >>
      strn "od" >> setbvs oldbvs))
 end
@@ -499,10 +499,6 @@ val enable_monadsyntax = add_monadsyntax
 val temp_enable_monadsyntax = temp_add_monadsyntax
 
 fun print_explicit_monadic_lets b = (explicit_mlets := b);
-fun set_monad_print_length NONE = (monad_print_length := ~1)
-  | set_monad_print_length (SOME n) =
-      if n < 0 then raise ERR "set_monad_print_length" "Cannot set a negative length!"
-      else (monad_print_length := n)
 
 val _ = TexTokenMap.temp_TeX_notation
             {hol = "<-", TeX = ("\\HOLTokenLeftmap{}", 1)}
diff --git a/src/prekernel/Globals.sig b/src/prekernel/Globals.sig
index 900d2d432f..714015708f 100644
--- a/src/prekernel/Globals.sig
+++ b/src/prekernel/Globals.sig
@@ -14,6 +14,7 @@ sig
   val show_scrub              : bool ref
   val linewidth               : int ref
   val max_print_depth         : int ref
+  val max_print_length        : int ref
   val type_pp_prefix          : string ref
   val type_pp_suffix          : string ref
   val term_pp_prefix          : string ref
diff --git a/src/prekernel/Globals.sml b/src/prekernel/Globals.sml
index e44345db7e..45a5f0425d 100644
--- a/src/prekernel/Globals.sml
+++ b/src/prekernel/Globals.sml
@@ -86,6 +86,12 @@ val max_print_depth = ref ~1
 
 val pp_flags = {show_types = ref false, show_numeral_types = ref false}
 
+(*---------------------------------------------------------------------------*
+ * Controls how many elements to print for list forms. Mirrors print depth.  *
+ *---------------------------------------------------------------------------*)
+
+val max_print_length = ref ~1
+
 (*---------------------------------------------------------------------------*
  * For prettyprinting type information in a term.                            *
  *---------------------------------------------------------------------------*)