Try to fix broken CI

hrutvik · hrutvik · commit fc009feac2d2 · 2025-03-31T17:08:53.000+01:00
diff --git a/compiler/parsing/pure_lexer_implScript.sml b/compiler/parsing/pure_lexer_implScript.sml
@@ -177,7 +177,7 @@ Theorem read_FFIcall_reduces_input:
      read_FFIcall s0 a l0 = (t, l, s) ⇒ LENGTH s < LENGTH s0 + 1
 Proof
   Induct >> dsimp[read_FFIcall_def, bool_case_eq] >> rw[] >>
-  qpat_x_assum `_ = _` (assume_tac o SYM) >> res_tac >> simp[]
+  res_tac >> gvs[]
 QED
 
 Definition next_sym_alt_def:
