equal
deleted
inserted
replaced
556 val reconstructor = Unsynchronized.ref "" |
556 val reconstructor = Unsynchronized.ref "" |
557 val named_thms = |
557 val named_thms = |
558 Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) |
558 Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) |
559 val minimize = AList.defined (op =) args minimizeK |
559 val minimize = AList.defined (op =) args minimizeK |
560 val metis_ft = AList.defined (op =) args metis_ftK |
560 val metis_ft = AList.defined (op =) args metis_ftK |
561 val trivial = Try.invoke_try (SOME try_timeout) pre |
561 val trivial = Try.invoke_try (SOME try_timeout) ([], [], []) pre |
562 handle TimeLimit.TimeOut => false |
562 handle TimeLimit.TimeOut => false |
563 fun apply_reconstructor m1 m2 = |
563 fun apply_reconstructor m1 m2 = |
564 if metis_ft |
564 if metis_ft |
565 then |
565 then |
566 if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false |
566 if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false |