src/Pure/Thy/term_style.ML
changeset 50637 81d6fe75ea5b
parent 50592 a39250169636
child 50638 eedc01eca736
     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) =