src/Pure/logic.ML

       if has_duplicates (eq_fst (op =)) tvars then err ()
       else map snd tvars;
   in (t, Ss, c) end;
 
 
-(* internalized sort constraints *)
+(* sort constraints within the logic *)
 
 fun dummy_tfree S = TFree ("'dummy", S);
 
 fun present_sorts shyps present_set =
   let