1structure thmpos_dtype = 2struct 3 4 5 datatype match_position 6 = Any 7 | Pat of Term.term Abbrev.quotation 8 | Pos of (Term.term list -> Term.term) 9 | Concl 10 11 12 13end (* struct *) 14