# HG changeset patch
# User wenzelm
# Date 1565601357 -7200
# Node ID 3f5d7fbaa1ea6171226f19a358de262d69199fca
# Parent  1881fb38a1ef8c53d7c5ead4c33d83ff8c1d1bef
tuned;

diff -r 1881fb38a1ef -r 3f5d7fbaa1ea src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Aug 12 11:04:41 2019 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Aug 12 11:15:57 2019 +0200
@@ -83,9 +83,10 @@
 
 (** FOL step Inference Rules **)
 
-fun lookth th_pairs fth =
-  the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
-  handle Option.Option => raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
+fun lookth th_pairs fol_th =
+  (case AList.lookup (uncurry Metis_Thm.equal) th_pairs fol_th of
+    SOME th => th
+  | NONE => raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fol_th))
 
 fun cterm_incr_types ctxt idx =
   Thm.cterm_of ctxt o map_types (Logic.incr_tvar idx)