equal
deleted
inserted
replaced
63 |
63 |
64 fun print_results true = Pretty.writeln oo pretty_results |
64 fun print_results true = Pretty.writeln oo pretty_results |
65 | print_results false = K (K ()); |
65 | print_results false = K (K ()); |
66 |
66 |
67 fun present_results ctxt ((kind, name), res) = |
67 fun present_results ctxt ((kind, name), res) = |
68 if kind = "" orelse kind = Drule.internalK then () |
68 if kind = "" orelse kind = PureThy.internalK then () |
69 else (print_results true ctxt ((kind, name), res); |
69 else (print_results true ctxt ((kind, name), res); |
70 Context.setmp (SOME (ProofContext.theory_of ctxt)) |
70 Context.setmp (SOME (ProofContext.theory_of ctxt)) |
71 (Present.results kind) (name_results name res)); |
71 (Present.results kind) (name_results name res)); |
72 |
72 |
73 end; |
73 end; |