tuned;

--- a/src/Pure/Thy/term_style.ML	Sun Dec 30 16:33:05 2012 +0100
+++ b/src/Pure/Thy/term_style.ML	Sun Dec 30 16:40:28 2012 +0100
@@ -65,9 +65,8 @@
     | _ => 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 =>
+val style_prem = Parse.nat >> (fn i => fn ctxt => fn t =>
   let
-    val i = (the o Int.fromString) raw_i;
     val prems = Logic.strip_imp_prems t;
   in
     if i <= length prems then nth prems (i - 1)