Fix overloading/holSyntaxExtraTheory

ordinarymath · ordinarymath · commit 4575c4ac4e67 · 2025-04-03T06:24:20.000Z
diff --git a/candle/overloading/syntax/holSyntaxExtraScript.sml b/candle/overloading/syntax/holSyntaxExtraScript.sml
@@ -8010,7 +8010,6 @@ Proof
           qpat_x_assum `!x. MEM _ (tyvars (Tyvar a)) \/ _ ==> ~MEM _ _` (qspec_then `a` mp_tac)
           >> rw[MEM_MAP,tyvars_def]
         )
-        >- fs[o_PAIR_MAP]
         >> CONV_TAC(RHS_CONV(PURE_ONCE_REWRITE_CONV [INSERT_SING_UNION]))
         >> fs[AC UNION_ASSOC UNION_COMM]
       )
@@ -8048,7 +8047,6 @@ Proof
         >> qpat_x_assum `!x. MEM _ (tyvars (Tyvar a)) \/ _ ==> ~MEM _ _` $ qspec_then `a` mp_tac
         >> rw[MEM_MAP,tyvars_def]
       )
-      >- fs[o_PAIR_MAP]
       >> CONV_TAC $ RHS_CONV $ PURE_ONCE_REWRITE_CONV [INSERT_SING_UNION]
       >> fs[AC UNION_ASSOC UNION_COMM]
     )

Original file line number	Diff line number	Diff line change
`@@ -8010,7 +8010,6 @@ Proof`
`8010`	`8010`	qpat_x_assum `!x. MEM _ (tyvars (Tyvar a)) \/ _ ==> ~MEM _ _` (qspec_then `a` mp_tac)
`8011`	`8011`	`>> rw[MEM_MAP,tyvars_def]`
`8012`	`8012`	`)`
`8013`		`- >- fs[o_PAIR_MAP]`
`8014`	`8013`	`>> CONV_TAC(RHS_CONV(PURE_ONCE_REWRITE_CONV [INSERT_SING_UNION]))`
`8015`	`8014`	`>> fs[AC UNION_ASSOC UNION_COMM]`
`8016`	`8015`	`)`
`@@ -8048,7 +8047,6 @@ Proof`
`8048`	`8047`	>> qpat_x_assum `!x. MEM _ (tyvars (Tyvar a)) \/ _ ==> ~MEM _ _` $ qspec_then `a` mp_tac
`8049`	`8048`	`>> rw[MEM_MAP,tyvars_def]`
`8050`	`8049`	`)`
`8051`		`- >- fs[o_PAIR_MAP]`
`8052`	`8050`	`>> CONV_TAC $ RHS_CONV $ PURE_ONCE_REWRITE_CONV [INSERT_SING_UNION]`
`8053`	`8051`	`>> fs[AC UNION_ASSOC UNION_COMM]`
`8054`	`8052`	`)`