From e67a01e80fd7910c40a1f4ea8d5e8803f63c2aad Mon Sep 17 00:00:00 2001
From: amblaf <chaster_killer@hotmail.fr>
Date: Thu, 25 Nov 2021 10:52:33 +0100
Subject: [PATCH] small bug fix in the heap relation generation

---
 c-refinement/Heap_Relation_Generation.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/c-refinement/Heap_Relation_Generation.thy b/c-refinement/Heap_Relation_Generation.thy
index 803f20799..877c535f9 100644
--- a/c-refinement/Heap_Relation_Generation.thy
+++ b/c-refinement/Heap_Relation_Generation.thy
@@ -49,7 +49,7 @@ fun mk_heap_rel ctxt (uvals:uval list) other prims =
   val rhs'' = mk_conjcts (ty_nm_Cs @ other)
 
   (* FIXME later: hey, Yutaka. rhs is a bit stupid.*)
-  val rhs= if (rhs' = []) orelse (rhs'' = []) then @{term "True"} else rhs'' @ rhs' |>mk_HOL_conjs ;
+  val rhs= if (rhs' = []) andalso (rhs'' = []) then @{term "True"} else rhs'' @ rhs' |>mk_HOL_conjs ;
   val heap_rel = Free ("heap_rel", dummyT);
   val lhs = strip_atype @{term "\<lambda> heap_rel . heap_rel \<sigma> h"} $ heap_rel |> strip_atype;
  in