equal
deleted
inserted
replaced
176 else if not (null nonmono_free_Ts) then "NONMONO" |
176 else if not (null nonmono_free_Ts) then "NONMONO" |
177 else "NIX" |
177 else "NIX" |
178 end |
178 end |
179 handle TimeLimit.TimeOut => "TIMEOUT" |
179 handle TimeLimit.TimeOut => "TIMEOUT" |
180 | NOT_SUPPORTED _ => "UNSUP" |
180 | NOT_SUPPORTED _ => "UNSUP" |
181 | _ => "UNKNOWN" |
181 | exn => if Exn.is_interrupt then reraise exn else "UNKNOWN" |
182 |
182 |
183 fun check_theory thy = |
183 fun check_theory thy = |
184 let |
184 let |
185 val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode) |
185 val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode) |
186 val _ = File.write path "" |
186 val _ = File.write path "" |