equal
deleted
inserted
replaced
386 val fc_b_name = Long_Name.base_name fcT_name; |
386 val fc_b_name = Long_Name.base_name fcT_name; |
387 val fc_b = Binding.name fc_b_name; |
387 val fc_b = Binding.name fc_b_name; |
388 |
388 |
389 fun qualify mandatory = Binding.qualify mandatory fc_b_name; |
389 fun qualify mandatory = Binding.qualify mandatory fc_b_name; |
390 |
390 |
391 fun dest_TFree_or_TVar (TFree sS) = sS |
|
392 | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S) |
|
393 | dest_TFree_or_TVar _ = error "Invalid type argument"; |
|
394 |
|
395 val (unsorted_As, B) = |
391 val (unsorted_As, B) = |
396 no_defs_lthy |
392 no_defs_lthy |
397 |> variant_tfrees (map (fst o dest_TFree_or_TVar) As0) |
393 |> variant_tfrees (map (fst o dest_TFree_or_TVar) As0) |
398 ||> the_single o fst o mk_TFrees 1; |
394 ||> the_single o fst o mk_TFrees 1; |
399 |
395 |