Closed yutakang closed 3 years ago
The name is already used in Pure/more_pattern.ML.
Pure/more_pattern.ML
Done in dad70e17dd810a00aaa2bfdcf7c7c920e835270c.
The name is already used in
Pure/more_pattern.ML
.