src/Pure/type_infer.ML
changeset 4270 957c887b89b5
parent 3784 3b15cda31c97
child 4957 30c49821e61f