diff --git a/thys/SpecCheck/Show/show_base.ML b/thys/SpecCheck/Show/show_base.ML
--- a/thys/SpecCheck/Show/show_base.ML
+++ b/thys/SpecCheck/Show/show_base.ML
@@ -1,47 +1,53 @@
 (*  Title:      SpecCheck/Show/show_base.ML
     Author:     Kevin Kappelmann
 
 Basic utility functions to create and combine show functions.
 *)
 
 signature SPECCHECK_SHOW_BASE =
 sig
   include SPECCHECK_SHOW_TYPES
 
   val none : 'a show
   val char : char show
   val string : string show
   val int : int show
   val real : real show
   val bool : bool show
   val list : 'a show -> ('a list) show
   val option : 'a show -> ('a option) show
 
   val zip : 'a show -> 'b show -> ('a * 'b) show
   val zip3 : 'a show -> 'b show -> 'c show -> ('a * 'b * 'c) show
   val zip4 : 'a show -> 'b show -> 'c show -> 'd show -> ('a * 'b * 'c * 'd) show
 
+  val record : ((string * Pretty.T) list) show
+
 end
 
 structure SpecCheck_Show_Base : SPECCHECK_SHOW_BASE =
 struct
 
 open SpecCheck_Show_Types
 
 fun none _ = Pretty.str "<NO_SHOW>"
 val char = Pretty.enclose "'" "'" o single o Pretty.str o Char.toString
 val string = Pretty.quote o Pretty.str
 val int = Pretty.str o string_of_int
 val real = Pretty.str o string_of_real
 fun bool b = Pretty.str (if b then "true" else "false")
 fun list show = Pretty.list "[" "]" o map show
 fun option _ NONE = Pretty.str "NONE"
   | option show (SOME v) = Pretty.block [Pretty.str "SOME ", show v]
 
 fun pretty_tuple ps = ps |> Pretty.commas |> Pretty.enclose "(" ")"
 
 fun zip showA showB (a, b) = pretty_tuple [showA a, showB b]
 fun zip3 showA showB showC (a, b, c) = pretty_tuple [showA a, showB b, showC c]
 fun zip4 showA showB showC showD (a, b, c, d) = pretty_tuple [showA a, showB b, showC c, showD d]
 
+val record =
+  map (fn (key, entry) => Pretty.block [Pretty.str key, Pretty.str "=", entry])
+  #> Pretty.enum "," "{" "}"
+
 end
diff --git a/thys/SpecCheck/Show/show_term.ML b/thys/SpecCheck/Show/show_term.ML
--- a/thys/SpecCheck/Show/show_term.ML
+++ b/thys/SpecCheck/Show/show_term.ML
@@ -1,54 +1,59 @@
 (*  Title:      SpecCheck/Show/show_term.ML
     Author:     Kevin Kappelmann
 
 Show functions for terms, types, and related data structures.
 *)
 
 signature SPECCHECK_SHOW_TERM =
 sig
 
   val term : Proof.context -> term SpecCheck_Show_Types.show
   val typ : Proof.context -> typ SpecCheck_Show_Types.show
   val thm : Proof.context -> thm SpecCheck_Show_Types.show
 
   val tyenv : Proof.context -> Type.tyenv SpecCheck_Show_Types.show
   val tenv : Proof.context -> Envir.tenv SpecCheck_Show_Types.show
   val env : Proof.context -> Envir.env SpecCheck_Show_Types.show
 
 end
 
 structure SpecCheck_Show_Term : SPECCHECK_SHOW_TERM =
 struct
 
 structure Show = SpecCheck_Show_Base
 
 val term = Syntax.pretty_term
 val typ = Syntax.pretty_typ
 fun thm ctxt = term ctxt o Thm.prop_of
 
 local 
 fun show_env_aux show_entry =
   Vartab.dest
   #> map show_entry
   #> Pretty.list "[" "]"
 
-fun show_env_entry show (s, t) = Pretty.enum " := " "" "" (map show [s, t])
+fun show_env_entry show (s, t) = Pretty.block [show s, Pretty.str " := ", show t]
+
 in
 
 fun tyenv ctxt =
   let
     val show_entry = show_env_entry (typ ctxt)
     fun get_typs (v, (s, T)) = (TVar (v, s), T)
   in show_env_aux (show_entry o get_typs) end
 
 fun tenv ctxt =
   let
     val show_entry = show_env_entry (term ctxt)
     fun get_trms (v, (T, t)) = (Var (v, T), t)
   in show_env_aux (show_entry o get_trms) end
 
 end
 
-fun env ctxt env = Show.zip (tyenv ctxt) (tenv ctxt) (Envir.type_env env, Envir.term_env env)
+fun env ctxt env = Show.record [
+    ("maxidx", Pretty.str (string_of_int (Envir.maxidx_of env))),
+    ("tyenv", tyenv ctxt (Envir.type_env env)),
+    ("tenv", tenv ctxt (Envir.term_env env))
+  ]
 
 end