Be more explicit with variable names to fix expk breakage

HOL-Theorem-Prover · Jun 23, 2016 · 75b3425 · 75b3425
1 parent e3d390e
commit 75b3425
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/examples/formal-languages/regular/regexpScript.sml b/examples/formal-languages/regular/regexpScript.sml
@@ -1431,6 +1431,7 @@ val SORTED_starts_charsets = Q.store_thm
  >- (fs [EVERY_MEM] >>
      Cases_on `rs1` >>
      fs [] >>
+     rename[`regexp_leq h _`] >>
      Cases_on `is_charset h`
      >- (qexists_tac `[h]` >>
          rw [])
@@ -1442,7 +1443,8 @@ val SORTED_starts_charsets = Q.store_thm
      >- (qexists_tac `[]` >>
          rw [] >>
          rw []))
- >- (qexists_tac `h::rs1` >>
+ >- (rename[`SORTED regexp_leq (h::(rs1++rs2))`] >>
+     qexists_tac `h::rs1` >>
      qexists_tac `rs2` >>
      rw [] >>
      Cases_on `rs1` >>