src/Pure/Proof/extraction.ML
changeset 35424 08c37d7bd2ad
parent 33957 e9afca2118d4
child 35845 e5980f0ad025
     1.1 --- a/src/Pure/Proof/extraction.ML	Mon Mar 01 21:41:35 2010 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Mar 02 22:18:51 2010 +0100
     1.3 @@ -207,9 +207,11 @@
     1.4    let val thy' = add_syntax thy
     1.5    in fn s =>
     1.6      let val t = Logic.varify (Syntax.read_prop_global thy' s)
     1.7 -    in (map Logic.dest_equals (Logic.strip_imp_prems t),
     1.8 -      Logic.dest_equals (Logic.strip_imp_concl t))
     1.9 -    end handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
    1.10 +    in
    1.11 +      (map Logic.dest_equals (Logic.strip_imp_prems t),
    1.12 +        Logic.dest_equals (Logic.strip_imp_concl t))
    1.13 +      handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
    1.14 +    end
    1.15    end;
    1.16  
    1.17  (** preprocessor **)