equal
deleted
inserted
replaced
573 SMT_Solver.smt_tac |
573 SMT_Solver.smt_tac |
574 else if full orelse !reconstructor = "metis (full_types)" then |
574 else if full orelse !reconstructor = "metis (full_types)" then |
575 Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] |
575 Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] |
576 else if !reconstructor = "metis (no_types)" then |
576 else if !reconstructor = "metis (no_types)" then |
577 Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] |
577 Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] |
|
578 else if !reconstructor = "metis" then |
|
579 Metis_Tactics.metis_tac [] |
578 else |
580 else |
579 Metis_Tactics.metis_tac []) ctxt thms |
581 K (K (K all_tac))) ctxt thms |
580 fun apply_reconstructor thms = |
582 fun apply_reconstructor thms = |
581 Mirabelle.can_apply timeout (do_reconstructor thms) st |
583 Mirabelle.can_apply timeout (do_reconstructor thms) st |
582 |
584 |
583 fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" |
585 fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" |
584 | with_time (true, t) = (change_data id (inc_reconstructor_success m); |
586 | with_time (true, t) = (change_data id (inc_reconstructor_success m); |