Fix rebinds

CakeML · Oct 19, 2023 · 9c3b012 · 9c3b012
1 parent 8f23342
commit 9c3b012
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 12 deletions.
diff --git 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
@@ -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