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