From d319ec50da09d7e60356354120a6a1e2ca1e4a67 Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Tue, 28 Nov 2023 15:25:02 +1100
Subject: [PATCH] Fixes for theories broken by 73dd13e64

---
 examples/lambda/other-models/MPlambdaScript.sml   | 2 +-
 examples/lambda/other-models/raw_syntaxScript.sml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/examples/lambda/other-models/MPlambdaScript.sml b/examples/lambda/other-models/MPlambdaScript.sml
index 220f05b1f8..483ead3307 100644
--- a/examples/lambda/other-models/MPlambdaScript.sml
+++ b/examples/lambda/other-models/MPlambdaScript.sml
@@ -1,5 +1,5 @@
 open HolKernel Parse boolLib bossLib binderLib
-open nomsetTheory
+open nomsetTheory horeductionTheory
 
 local open stringTheory in end
 
diff --git a/examples/lambda/other-models/raw_syntaxScript.sml b/examples/lambda/other-models/raw_syntaxScript.sml
index f6c1f04666..548b1d1ae3 100644
--- a/examples/lambda/other-models/raw_syntaxScript.sml
+++ b/examples/lambda/other-models/raw_syntaxScript.sml
@@ -3,7 +3,7 @@ open HolKernel Parse boolLib bossLib BasicProvers metisLib
 local open stringTheory in end
 
 open pred_setTheory binderLib boolSimps relationTheory
-open chap3Theory
+open horeductionTheory chap3Theory
 
 (* ----------------------------------------------------------------------