src/HOL/Tools/Metis/metis_tactics.ML
changeset 42733 01ef1c3d9cfd
parent 42650 552eae49f97d
child 42739 017e5dac8642
     1.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu May 12 15:29:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu May 12 15:29:19 2011 +0200
     1.3 @@ -122,7 +122,15 @@
     1.4               else
     1.5                 ();
     1.6               [])
     1.7 -  end;
     1.8 +  end
     1.9 +  handle METIS (loc, msg) =>
    1.10 +         if mode <> FT then
    1.11 +           (verbose_warning ctxt ("Falling back on \"metisFT\".");
    1.12 +            FOL_SOLVE FT ctxt cls ths0)
    1.13 +         else
    1.14 +           error ("Failed to replay Metis proof in Isabelle." ^
    1.15 +                  (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
    1.16 +                   else ""))
    1.17  
    1.18  (* Extensionalize "th", because that makes sense and that's what Sledgehammer
    1.19     does, but also keep an unextensionalized version of "th" for backward
    1.20 @@ -163,15 +171,6 @@
    1.21        Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
    1.22                    (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
    1.23                    ctxt i st0
    1.24 -      handle METIS (loc, msg) =>
    1.25 -             if mode <> FT then
    1.26 -               (verbose_warning ctxt ("Falling back on \"metisFT\".");
    1.27 -                generic_metis_tac FT ctxt ths i st0)
    1.28 -             else
    1.29 -               error ("Failed to replay Metis proof in Isabelle." ^
    1.30 -                      (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
    1.31 -                       else ""))
    1.32 -
    1.33    end
    1.34  
    1.35  val metis_tac = generic_metis_tac HO