equal
deleted
inserted
replaced
350 Name_Space.markup (fixes_space ctxt) x |
350 Name_Space.markup (fixes_space ctxt) x |
351 |> Markup.name (revert_fixed ctxt x); |
351 |> Markup.name (revert_fixed ctxt x); |
352 |
352 |
353 fun dest_fixes ctxt = |
353 fun dest_fixes ctxt = |
354 Name_Space.fold_table (fn (x, y) => cons (y, x)) (fixes_of ctxt) [] |
354 Name_Space.fold_table (fn (x, y) => cons (y, x)) (fixes_of ctxt) [] |
355 |> sort (Name_Space.entry_ord (fixes_space ctxt) o pairself #2); |
355 |> sort (Name_Space.entry_ord (fixes_space ctxt) o apply2 #2); |
356 |
356 |
357 |
357 |
358 (* collect variables *) |
358 (* collect variables *) |
359 |
359 |
360 fun add_free_names ctxt = |
360 fun add_free_names ctxt = |
401 val _ = |
401 val _ = |
402 (case filter (Name.is_skolem o Binding.name_of) bs of |
402 (case filter (Name.is_skolem o Binding.name_of) bs of |
403 [] => () |
403 [] => () |
404 | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads))); |
404 | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads))); |
405 val _ = |
405 val _ = |
406 (case duplicates (op = o pairself Binding.name_of) bs of |
406 (case duplicates (op = o apply2 Binding.name_of) bs of |
407 [] => () |
407 [] => () |
408 | dups => err_dups dups); |
408 | dups => err_dups dups); |
409 |
409 |
410 val xs = map check_name bs; |
410 val xs = map check_name bs; |
411 val names = names_of ctxt; |
411 val names = names_of ctxt; |