equal
deleted
inserted
replaced
597 fun uncheck_case ctxt ts = |
597 fun uncheck_case ctxt ts = |
598 if Config.get ctxt show_cases |
598 if Config.get ctxt show_cases |
599 then map (fn t => if can Term.type_of t then strip_case_full ctxt true t else t) ts |
599 then map (fn t => if can Term.type_of t then strip_case_full ctxt true t else t) ts |
600 else ts; |
600 else ts; |
601 |
601 |
602 val _ = Context.>> (Syntax_Phases.term_uncheck 1 "case" uncheck_case); |
602 val _ = Context.>> (Syntax_Phases.term_uncheck 1 "case" uncheck_case); |
603 |
603 |
604 |
604 |
605 (* outer syntax commands *) |
605 (* outer syntax commands *) |
606 |
606 |
607 fun print_case_translations ctxt = |
607 fun print_case_translations ctxt = |