From 9c3b0129d9c323a506d252eab9ab798c0561997a Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Thu, 19 Oct 2023 10:11:55 +0200
Subject: [PATCH] Fix rebinds

---
 .../semantics/holModelConservativityScript.sml        |  2 +-
 .../overloading/semantics/holSemanticsExtraScript.sml | 11 -----------
 2 files changed, 1 insertion(+), 12 deletions(-)

diff --git a/candle/overloading/semantics/holModelConservativityScript.sml b/candle/overloading/semantics/holModelConservativityScript.sml
index d68cb4f907..6b68067290 100644
--- a/candle/overloading/semantics/holModelConservativityScript.sml
+++ b/candle/overloading/semantics/holModelConservativityScript.sml
@@ -1629,7 +1629,7 @@ Proof
   simp[] >>
   drule_then match_mp_tac RTC_RTC >>
   match_mp_tac RTC_SUBSET >>
-  simp[subtype1_def]
+  simp[subtype1_cases]
 QED
 
 (* the independent fragment of an update's dependencies
diff --git a/candle/overloading/semantics/holSemanticsExtraScript.sml b/candle/overloading/semantics/holSemanticsExtraScript.sml
index 215bf457ef..6b9e125586 100644
--- a/candle/overloading/semantics/holSemanticsExtraScript.sml
+++ b/candle/overloading/semantics/holSemanticsExtraScript.sml
@@ -453,17 +453,6 @@ Proof
   rw[GSYM IMP_DISJ_THM] >> fs[LIST_TO_SET_MAP]
 QED
 
-Theorem type_ok_TYPE_SUBSTf:
- !r sig sigma. (∀ty. tyvars (sigma ty) = []) /\
-  (∀ty. type_ok sig (sigma ty)) /\
-  type_ok sig r ==>
-  type_ok sig (TYPE_SUBSTf sigma r)
-Proof
-  ho_match_mp_tac type_ind >> rpt strip_tac
-  >- simp[type_ok_def]
-  >> fs[EVERY_MEM,type_ok_def,MEM_MAP,PULL_EXISTS]
-QED
-
 Theorem consts_of_term_ok:
   !tm q r. term_ok sig tm /\ (q,r) ∈ consts_of_term tm ==> type_ok (tysof sig) r
 Proof