From 754414b1e27a33ce3c216e4544a3f83ba9d82d62 Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Thu, 22 Jun 2023 08:42:54 +1000
Subject: [PATCH] Fix another parse error in Theorem-Proof syntax

---
 examples/lpr_checker/lpr_parsingScript.sml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/examples/lpr_checker/lpr_parsingScript.sml b/examples/lpr_checker/lpr_parsingScript.sml
index 1a562de0c5..b974ad39ac 100644
--- 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>>