more precise scope of exception handler;

--- 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 **)