From e9f42788c98b50c5ed243cde1d13f9a8365e76ea Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 23 Sep 2024 17:02:56 +0200 Subject: [PATCH] fix --- src/boss/prove_base_assumsScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/boss/prove_base_assumsScript.sml b/src/boss/prove_base_assumsScript.sml index cdd98e520c..b3c8c53bf6 100644 --- a/src/boss/prove_base_assumsScript.sml +++ b/src/boss/prove_base_assumsScript.sml @@ -123,7 +123,7 @@ val (reader:reader) = { val base_thms = read_article "base-theorems.art" reader; -val _ = Net.itnet Thm.delete_proof base_thms (); +val base_thms = Net.map Thm.delete_proof base_thms; fun itpred P th acc = if P th then th::acc else acc; fun amatch tm = Net.itnet (itpred (DB.matches tm)) base_thms [];