src/Pure/type_infer.ML
changeset 23597 ab67175ca8a5
parent 22771 ce1fe6ca7dbb
child 24275 bbc3dab6d4fe