--- a/thys/Simpl/hoare_syntax.ML
+++ b/thys/Simpl/hoare_syntax.ML
@@ -1247,7 +1247,7 @@
         then (I, t') (* Get rid of last abstraction *)
         else (fn t => Abs (x, T, recomb t), t')
      end
-  | split_Let' ((s as Const (@{const_syntax split},_)) $ t) =
+  | split_Let' ((s as Const (@{const_syntax prod_case},_)) $ t) =
      let val (recomb, t') = split_Let' t
      in (fn t => s $ recomb t, t') end
   | split_Let' t = (I, t)