small bug fix in the heap relation generation

au-ts · Nov 25, 2021 · e67a01e · e67a01e
1 parent dcf2cf8
commit e67a01e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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