# HG changeset patch # User wenzelm # Date 1356881585 -3600 # Node ID 81d6fe75ea5b3f0d742712010c59d8255e5c2329 # Parent 07f47142378e850ba965bf4af74cb742e370173f tuned whitespace; diff -r 07f47142378e -r 81d6fe75ea5b src/Pure/Thy/term_style.ML --- a/src/Pure/Thy/term_style.ML Sun Dec 30 16:23:30 2012 +0100 +++ b/src/Pure/Thy/term_style.ML Sun Dec 30 16:33:05 2012 +0100 @@ -47,7 +47,7 @@ (Scan.lift (the_style (Proof_Context.theory_of ctxt) name)) (Args.src x) ctxt |>> (fn f => f ctxt))); -val parse = Args.context :|-- (fn ctxt => Scan.lift +val parse = Args.context :|-- (fn ctxt => Scan.lift (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt)) >> fold I || Scan.succeed I)); @@ -60,8 +60,9 @@ val concl = Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t) in - case concl of (_ $ l $ r) => proj (l, r) - | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl) + (case concl of + (_ $ l $ r) => proj (l, r) + | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)) end); val style_prem = Args.name >> (fn raw_i => fn ctxt => fn t => @@ -70,8 +71,9 @@ val prems = Logic.strip_imp_prems t; in if i <= length prems then nth prems (i - 1) - else error ("Not enough premises for prem " ^ string_of_int i ^ - " in propositon: " ^ Syntax.string_of_term ctxt t) + else + error ("Not enough premises for prem " ^ string_of_int i ^ + " in propositon: " ^ Syntax.string_of_term ctxt t) end); fun isub_symbols (d :: s :: ss) = diff -r 07f47142378e -r 81d6fe75ea5b src/Pure/library.ML --- a/src/Pure/library.ML Sun Dec 30 16:23:30 2012 +0100 +++ b/src/Pure/library.ML Sun Dec 30 16:33:05 2012 +0100 @@ -668,9 +668,9 @@ val limit = zero + radix; fun scan (num, []) = (num, []) | scan (num, c :: cs) = - if zero <= ord c andalso ord c < limit then - scan (radix * num + (ord c - zero), cs) - else (num, c :: cs); + if zero <= ord c andalso ord c < limit then + scan (radix * num + (ord c - zero), cs) + else (num, c :: cs); in scan (0, cs) end; val read_int = read_radix_int 10;