src/Pure/Thy/term_style.ML
changeset 50638 eedc01eca736
parent 50637 81d6fe75ea5b
child 53021 d0fa3f446b9d
     1.1 --- a/src/Pure/Thy/term_style.ML	Sun Dec 30 16:33:05 2012 +0100
     1.2 +++ b/src/Pure/Thy/term_style.ML	Sun Dec 30 16:40:28 2012 +0100
     1.3 @@ -65,9 +65,8 @@
     1.4      | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl))
     1.5    end);
     1.6  
     1.7 -val style_prem = Args.name >> (fn raw_i => fn ctxt => fn t =>
     1.8 +val style_prem = Parse.nat >> (fn i => fn ctxt => fn t =>
     1.9    let
    1.10 -    val i = (the o Int.fromString) raw_i;
    1.11      val prems = Logic.strip_imp_prems t;
    1.12    in
    1.13      if i <= length prems then nth prems (i - 1)