From 7101a3f2e0c3885412c05e63735ec6da155253ee Mon Sep 17 00:00:00 2001
From: Magnus Myreen <magnus.myreen@cl.cam.ac.uk>
Date: Wed, 8 Nov 2023 22:36:03 +0100
Subject: [PATCH] Fix for adjusted Inductive syntax

---
 candle/prover/candle_kernel_valsScript.sml |  6 ++---
 candle/prover/candle_prover_invScript.sml  | 26 +++++++++++-----------
 2 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/candle/prover/candle_kernel_valsScript.sml b/candle/prover/candle_kernel_valsScript.sml
index ac198f0f28..6c9a7a5548 100644
--- a/candle/prover/candle_kernel_valsScript.sml
+++ b/candle/prover/candle_kernel_valsScript.sml
@@ -167,17 +167,17 @@ Inductive inferred:
 [~KernelFuns:]
   (∀ctxt f.
      f ∈ kernel_funs ⇒
-       inferred ctxt f) ∧
+       inferred ctxt f)
 [~TYPE:]
   (∀ctxt ty v.
      TYPE ctxt ty ∧
      TYPE_TYPE ty v ⇒
-       inferred ctxt v) ∧
+       inferred ctxt v)
 [~TERM:]
   (∀ctxt tm v.
      TERM ctxt tm ∧
      TERM_TYPE tm v ⇒
-       inferred ctxt v) ∧
+       inferred ctxt v)
 [~THM:]
   (∀ctxt th v.
      THM ctxt th ∧
diff --git a/candle/prover/candle_prover_invScript.sml b/candle/prover/candle_prover_invScript.sml
index 70c2c098ec..b8a1b91975 100644
--- a/candle/prover/candle_prover_invScript.sml
+++ b/candle/prover/candle_prover_invScript.sml
@@ -78,56 +78,56 @@ Inductive v_ok:
 [~Inferred:]
   (∀ctxt v.
      inferred ctxt v ⇒
-       kernel_vals ctxt v) ∧
+       kernel_vals ctxt v)
 [~PartialApp:]
   (∀ctxt f v g.
      kernel_vals ctxt f ∧
      v_ok ctxt v ∧
      do_partial_app f v = SOME g ⇒
-       kernel_vals ctxt g) ∧
+       kernel_vals ctxt g)
 [~KernelVals:]
   (∀ctxt v.
      kernel_vals ctxt v ⇒
-       v_ok ctxt v) ∧
+       v_ok ctxt v)
 [~Conv:]
   (∀ctxt opt vs.
      EVERY (v_ok ctxt) vs ∧
      (∀tag x. opt = SOME (TypeStamp tag x) ⇒ x ∉ kernel_types) ⇒
-       v_ok ctxt (Conv opt vs)) ∧
+       v_ok ctxt (Conv opt vs))
 [~Closure:]
   (∀ctxt env n x.
      env_ok ctxt env ∧
      safe_exp x ⇒
-       v_ok ctxt (Closure env n x)) ∧
+       v_ok ctxt (Closure env n x))
 [~Recclosure:]
   (∀ctxt env f n.
      env_ok ctxt env ∧
      EVERY safe_exp (MAP (SND o SND) f) ⇒
-       v_ok ctxt (Recclosure env f n)) ∧
+       v_ok ctxt (Recclosure env f n))
 [~Vectorv:]
   (∀ctxt vs.
      EVERY (v_ok ctxt) vs ⇒
-       v_ok ctxt (Vectorv vs)) ∧
+       v_ok ctxt (Vectorv vs))
 [~Lit:]
   (∀ctxt lit.
-     v_ok ctxt (Litv lit)) ∧
+     v_ok ctxt (Litv lit))
 [~FP_WordTree:]
   (∀ ctxt fp.
-     v_ok ctxt (FP_WordTree fp)) ∧
+     v_ok ctxt (FP_WordTree fp))
 [~FP_BoolTree:]
   (∀ ctxt fp.
-     v_ok ctxt (FP_BoolTree fp)) ∧
+     v_ok ctxt (FP_BoolTree fp))
 [~Real:]
   (∀ ctxt r.
-     v_ok ctxt (Real r)) ∧
+     v_ok ctxt (Real r))
 [~Loc:]
   (∀ctxt loc.
      loc ∉ kernel_locs ⇒
-       v_ok ctxt (Loc loc)) ∧
+       v_ok ctxt (Loc loc))
 [~Env:]
   (∀ctxt env ns.
      env_ok ctxt env ⇒
-       v_ok ctxt (Env env ns)) ∧
+       v_ok ctxt (Env env ns))
 [env_ok:]
   (∀ctxt env.
      (∀id len tag tn.