# HG changeset patch
# User wenzelm
# Date 1267564731 -3600
# Node ID 08c37d7bd2ad6179ac98e52d2eeff9c9b377bd7d
# Parent  6ef9525a57270bef94b2aed67d43d14cd5c99b46
more precise scope of exception handler;

diff -r 6ef9525a5727 -r 08c37d7bd2ad src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Mar 01 21:41:35 2010 +0100
+++ b/src/Pure/Proof/extraction.ML	Tue Mar 02 22:18:51 2010 +0100
@@ -207,9 +207,11 @@
   let val thy' = add_syntax thy
   in fn s =>
     let val t = Logic.varify (Syntax.read_prop_global thy' s)
-    in (map Logic.dest_equals (Logic.strip_imp_prems t),
-      Logic.dest_equals (Logic.strip_imp_concl t))
-    end handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
+    in
+      (map Logic.dest_equals (Logic.strip_imp_prems t),
+        Logic.dest_equals (Logic.strip_imp_concl t))
+      handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
+    end
   end;
 
 (** preprocessor **)