From 2dca0755beab1b40e449b6c343da4c5ec176c75e Mon Sep 17 00:00:00 2001
From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com>
Date: Mon, 23 Sep 2024 16:27:37 +0200
Subject: [PATCH] Fix error

I honestly have no idea how that happened.
---
 characteristic/cfScript.sml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/characteristic/cfScript.sml b/characteristic/cfScript.sml
index efd917a89b..4816d18cbe 100644
--- a/characteristic/cfScript.sml
+++ b/characteristic/cfScript.sml
@@ -2000,8 +2000,7 @@ Definition cf_def:
   cf (p:'ffi ffi_proj) (Tannot e _) = cf p e /\
   cf _ _ = cf_bottom
 Termination
-  WF_REL_TAC
-Endmeasure (exp_size o SND)` \\ rw []
+  WF_REL_TAC `measure (exp_size o SND)` \\ rw []
     THEN1 (
       Cases_on `opt` \\ Cases_on `e1` \\ fs [is_bound_Fun_def] \\
       drule Fun_body_exp_size \\ strip_tac \\ fs [astTheory.exp_size_def]
@@ -2014,7 +2013,6 @@ Endmeasure (exp_size o SND)` \\ rw []
       drule Fun_body_exp_size \\ strip_tac \\ fs [astTheory.exp_size_def]
     )
 End
-
 val cf_defs = [
   cf_def,
   cf_lit_def,