Fix another parse error in Theorem-Proof syntax

CakeML · Jun 21, 2023 · 754414b · 754414b
1 parent ca3e595
commit 754414b
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/examples/lpr_checker/lpr_parsingScript.sml b/examples/lpr_checker/lpr_parsingScript.sml
@@ -484,10 +484,11 @@ val parse_until_nn_def = Define`
       parse_until_nn xs (Num l::acc)
   )`
 
-val parse_until_nn_length = Q.prove(`
+Theorem parse_until_nn_length[local]:
   ∀ls acc a b c.
   parse_until_nn ls acc = SOME(a,b,c) ⇒
-  LENGTH c < LENGTH ls`,
+  LENGTH c < LENGTH ls
+Proof
   Induct>>fs[parse_until_nn_def]>>
   rw[]>>every_case_tac>>fs[]>>
   first_x_assum drule>>