Correct proof failure caused by change to irule in HOL

CakeML · May 29, 2018 · 1337e80 · 1337e80
1 parent 5b0e7d5
commit 1337e80
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/semantics/proofs/typeSysPropsScript.sml b/semantics/proofs/typeSysPropsScript.sml
@@ -2304,7 +2304,7 @@ val type_specs_tenv_ok = Q.store_thm ("type_specs_tenv_ok",
  >- (
    `tenv_abbrev_ok (nsSing tn (tvs,Tapp (MAP Tvar tvs) (TC_name (mk_id mn tn))))`
      by simp [tenv_abbrev_ok_def, check_freevars_def, EVERY_MEM, EVERY_MAP]
-   >> irule extend_dec_tenv_ok
+   >> irule extend_dec_tenv_ok >> conj_tac
    >- (
      first_x_assum irule
      >> simp [tenv_abbrev_ok_def]