From ca3e595e8ff524933b16be2b8004025b16afb935 Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Wed, 21 Jun 2023 11:34:16 +1000
Subject: [PATCH] Fix a Theorem-Proof-QED error now flagged by most recent HOL

---
 characteristic/examples/cf_examplesScript.sml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/characteristic/examples/cf_examplesScript.sml b/characteristic/examples/cf_examplesScript.sml
index c35d3000dd..823cacf13c 100644
--- a/characteristic/examples/cf_examplesScript.sml
+++ b/characteristic/examples/cf_examplesScript.sml
@@ -143,7 +143,7 @@ Proof
   xcf' "is_none" \\ Cases_on `opt` \\
   fs [OPTION_TYPE_def] \\
   xmatch \\ xcon \\ xsimpl
-)
+QED
 
 val example_eq = (append_prog o process_topdecs)
   `fun example_eq x = (x = 3)`