tuned whitespace;
authorwenzelm
Sun Dec 30 16:33:05 2012 +0100 (2012-12-30)
changeset 5063781d6fe75ea5b
parent 50636 07f47142378e
child 50638 eedc01eca736
tuned whitespace;
src/Pure/Thy/term_style.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/Thy/term_style.ML	Sun Dec 30 16:23:30 2012 +0100
     1.2 +++ b/src/Pure/Thy/term_style.ML	Sun Dec 30 16:33:05 2012 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4         (Scan.lift (the_style (Proof_Context.theory_of ctxt) name))
     1.5           (Args.src x) ctxt |>> (fn f => f ctxt)));
     1.6  
     1.7 -val parse = Args.context :|-- (fn ctxt => Scan.lift 
     1.8 +val parse = Args.context :|-- (fn ctxt => Scan.lift
     1.9    (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt))
    1.10        >> fold I
    1.11    || Scan.succeed I));
    1.12 @@ -60,8 +60,9 @@
    1.13      val concl =
    1.14        Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)
    1.15    in
    1.16 -    case concl of (_ $ l $ r) => proj (l, r)
    1.17 -    | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
    1.18 +    (case concl of
    1.19 +      (_ $ l $ r) => proj (l, r)
    1.20 +    | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl))
    1.21    end);
    1.22  
    1.23  val style_prem = Args.name >> (fn raw_i => fn ctxt => fn t =>
    1.24 @@ -70,8 +71,9 @@
    1.25      val prems = Logic.strip_imp_prems t;
    1.26    in
    1.27      if i <= length prems then nth prems (i - 1)
    1.28 -    else error ("Not enough premises for prem " ^ string_of_int i ^
    1.29 -      " in propositon: " ^ Syntax.string_of_term ctxt t)
    1.30 +    else
    1.31 +      error ("Not enough premises for prem " ^ string_of_int i ^
    1.32 +        " in propositon: " ^ Syntax.string_of_term ctxt t)
    1.33    end);
    1.34  
    1.35  fun isub_symbols (d :: s :: ss) =
     2.1 --- a/src/Pure/library.ML	Sun Dec 30 16:23:30 2012 +0100
     2.2 +++ b/src/Pure/library.ML	Sun Dec 30 16:33:05 2012 +0100
     2.3 @@ -668,9 +668,9 @@
     2.4      val limit = zero + radix;
     2.5      fun scan (num, []) = (num, [])
     2.6        | scan (num, c :: cs) =
     2.7 -        if zero <= ord c andalso ord c < limit then
     2.8 -          scan (radix * num + (ord c - zero), cs)
     2.9 -        else (num, c :: cs);
    2.10 +          if zero <= ord c andalso ord c < limit then
    2.11 +            scan (radix * num + (ord c - zero), cs)
    2.12 +          else (num, c :: cs);
    2.13    in scan (0, cs) end;
    2.14  
    2.15  val read_int = read_radix_int 10;