diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index c60fa53678..583b07cbb1 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -358,13 +358,6 @@ module Transition = (EV: EV_MODE) => {
             is_value: false,
           });
         }
-      // let.match env'' = (env', matches(dp, d2'));
-      // Step({
-      //   expr: Closure(env'', d3) |> fresh,
-      //   state_update,
-      //   kind: FunAp,
-      //   is_value: false,
-      // });
       | Cast(
           d3',
           {term: Arrow(ty1, ty2), _},
@@ -783,6 +776,8 @@ module Transition = (EV: EV_MODE) => {
       let. _ = otherwise(env, d);
       Indet;
     | Parens(d'', Probe(pr)) =>
+      /* When evaluated, a probe adds a dynamics info entry
+       * reflecting the evaluation of the contained expression */
       let. _ = otherwise(env, ((d, _)) => Parens(d, Probe(pr)) |> rewrap)
       and. (d', _) =
         req_final_or_value(
diff --git a/src/haz3lcore/pretty/ExpToSegment.re b/src/haz3lcore/pretty/ExpToSegment.re
index c11da79308..f1e3791856 100644
--- a/src/haz3lcore/pretty/ExpToSegment.re
+++ b/src/haz3lcore/pretty/ExpToSegment.re
@@ -49,7 +49,9 @@ let should_add_space = (s1, s2) =>
         && !Form.is_keyword(s1)
         && String.starts_with(s2, ~prefix="(") =>
     false
-  | _ when String.ends_with(s1, ~suffix="…") => false
+  | _ when String.ends_with(s1, ~suffix="…") =>
+    /* Hack case for probe projector abbreviations */
+    false
   | _ => true
   };
 
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index 1a651ec1de..38c00f5951 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -15,7 +15,7 @@ open Any;
 
 /* Hack: Temporary construct internal to maketerm
  * to handle probe parsing; see `tokens` below */
-let probe_wrap = ["@@@@@", "@@@@@"];
+let probe_wrap = ["PROBE_WRAP", "PROBE_WRAP"];
 let is_probe_wrap = (==)(probe_wrap);
 
 // TODO make less hacky
@@ -545,10 +545,7 @@ and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => {
     | Grout(_) => []
     | Projector({syntax, id: _, _}) =>
       let sort = Piece.sort(syntax) |> fst;
-      let seg = [syntax];
-      //let seg = [mk_probe(id, seg)];
-      //print_endline("unsorted projector case");
-      [go_s(sort, Segment.skel(seg), seg)];
+      [go_s(sort, Segment.skel([syntax]), [syntax])];
     | Tile({mold, shards, children, _}) =>
       Aba.aba_triples(Aba.mk(shards, children))
       |> List.map(((l, kid, r)) => {
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index ac8dcdb122..f20e3f8e57 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -1,29 +1,29 @@
 /* STATICS.re
 
-    This module determines the statics semantics of a program.
-    It makes use of the following modules:
+   This module determines the statics semantics of a program.
+   It makes use of the following modules:
 
-    INFO.re: Defines the Info.t type which is used to represent the
-    static STATUS of a term. This STATUS can be either OK or ERROR,
-    and is determined by reconcilling two sources of typing information,
-    the MODE and the SELF.
+   INFO.re: Defines the Info.t type which is used to represent the
+   static STATUS of a term. This STATUS can be either OK or ERROR,
+   and is determined by reconcilling two sources of typing information,
+   the MODE and the SELF.
 
-    MODE.re: Defines the Mode.t type which is used to represent the
-    typing expectations imposed by a term's ancestors.
+   MODE.re: Defines the Mode.t type which is used to represent the
+   typing expectations imposed by a term's ancestors.
 
-    SELF.re: Define the Self.t type which is used to represent the
-    type information derivable from the term itself.
+   SELF.re: Define the Self.t type which is used to represent the
+   type information derivable from the term itself.
 
-    The point of STATICS.re itself is to derive a map between each
-    term's unique id and that term's static INFO. The below functions
-    are intended mostly as infrastructure: The point is to define a
-    traversal through the syntax tree which, for each term, passes
-    down the MODE, passes up the SELF, calculates the INFO, and adds
-    it to the map.
+   The point of STATICS.re itself is to derive a map between each
+   term's unique id and that term's static INFO. The below functions
+   are intended mostly as infrastructure: The point is to define a
+   traversal through the syntax tree which, for each term, passes
+   down the MODE, passes up the SELF, calculates the INFO, and adds
+   it to the map.
 
-    The architectural intention here is that most type-manipulation
-    logic is defined in INFO, MODE, and SELF, and the STATICS module
-    itself is dedicated to the piping necessary to (A) introduce and
+   The architectural intention here is that most type-manipulation
+   logic is defined in INFO, MODE, and SELF, and the STATICS module
+   itself is dedicated to the piping necessary to (A) introduce and
    (B) propagate the necessary information through the syntax tree.
 
      */
diff --git a/src/haz3lweb/app/editors/result/EvalResult.re b/src/haz3lweb/app/editors/result/EvalResult.re
index 62f655a7ab..840f2b0961 100644
--- a/src/haz3lweb/app/editors/result/EvalResult.re
+++ b/src/haz3lweb/app/editors/result/EvalResult.re
@@ -93,7 +93,7 @@ module Model = {
     switch (model.result) {
     | Evaluation({result: OldValue(ResultOk((_, state))), _})
     | Evaluation({result: NewValue(ResultOk((_, state))), _}) =>
-      Some(state |> Haz3lcore.EvaluatorState.get_probes)
+      Some(Haz3lcore.EvaluatorState.get_probes(state))
     | Stepper(s) =>
       Some(
         s.history