Skip to content

Commit 9b4dc3d

Browse files
Fix breakage from HOL update in std_prelude
1 parent edb9197 commit 9b4dc3d

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

translator/ml_translatorScript.sml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1707,8 +1707,8 @@ QED
17071707
(* pair definition *)
17081708

17091709
Definition PAIR_TYPE_def:
1710-
PAIR_TYPE b c (x_2:'b,x_1:'c) v <=>
1711-
?v1_1 v1_2. v = Conv NONE [v1_1; v1_2] /\ b x_2 v1_1 /\ c x_1 v1_2
1710+
PAIR_TYPE a b (x_2:'a,x_1:'b) v <=>
1711+
?v1_1 v1_2. v = Conv NONE [v1_1; v1_2] /\ a x_2 v1_1 /\ b x_1 v1_2
17121712
End
17131713

17141714
val PAIR_TYPE_SIMP = Q.prove(

0 commit comments

Comments
 (0)