equal
deleted
inserted
replaced
601 fun make_def_binding cond b = if cond then def_binding b else Binding.empty; |
601 fun make_def_binding cond b = if cond then def_binding b else Binding.empty; |
602 |
602 |
603 |
603 |
604 (* unofficial theorem names *) |
604 (* unofficial theorem names *) |
605 |
605 |
|
606 fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN; |
606 fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); |
607 fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); |
607 |
608 fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown"; |
608 val has_name_hint = can the_name_hint; |
|
609 val get_name_hint = the_default "??.unknown" o try the_name_hint; |
|
610 |
609 |
611 fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); |
610 fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); |
612 |
611 |
613 |
612 |
614 (* theorem kinds *) |
613 (* theorem kinds *) |