fix failure in cnf_xor

CakeML · Feb 8, 2024 · 2531d2c · 2531d2c
1 parent e0b389a
commit 2531d2c
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/examples/xlrup_checker/cnf_xorScript.sml b/examples/xlrup_checker/cnf_xorScript.sml
@@ -329,10 +329,8 @@ Proof
   drule fromString_print_lit>>
   rw[]>>simp[]>>
   qmatch_goalsub_abbrev_tac`ll::acc`>>
-  qsuff_tac`ll=h`>>rw[]
-  >-
-    (first_x_assum drule>>simp[])>>
-  simp[Abbr`ll`]>>every_case_tac>>fs[]
+  gvs[]>>
+  Cases_on`h`>>gvs[var_lit_def]
 QED
 
 Theorem parse_clause_print_clause: