switch back to metis proof for stability

halbGefressen · Sep 23, 2024 · f7f6839 · f7f6839
1 parent 1769c35
commit f7f6839
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/flatinduct.ML b/flatinduct.ML
@@ -77,7 +77,7 @@ fun flatinduct ctxt t =
   let val ((vars, t), ctxt') = (Variable.import true [t] ctxt) |>> (I ##> hd)
       val tactic = (fn _ => (* by (rule t) (metis (no_types))+ *)
         (resolve_tac ctxt' [Thm.instantiate vars t] 1) THEN
-         REPEAT (SMT_Solver.smt_tac ctxt' [] 1))
+         REPEAT (metis_default_tac ctxt'))
       val proven = Goal.prove ctxt [] [] (flatinduct_rewrite ctxt t) tactic
   in singleton (Variable.export ctxt' ctxt) proven
   end