src/Pure/Isar/term_style.ML
changeset 16165 dbe9ee8ffcdd
parent 16160 833f4160130e
child 16167 b2e4c4058b71
--- a/src/Pure/Isar/term_style.ML	Wed Jun 01 09:46:06 2005 +0200
+++ b/src/Pure/Isar/term_style.ML	Wed Jun 01 10:30:07 2005 +0200
@@ -59,7 +59,7 @@
 
 fun premise i _ t =
   let val prems = Logic.strip_imp_prems t
-  in if i <= length prems then List.nth(prems,i-1)
+  in if i <= length prems then List.nth(prems, i-1)
      else error ("Not enough premises: premise" ^ string_of_int i)
   end;
  
@@ -75,6 +75,6 @@
   add_style "premise7" (premise 7),
   add_style "premise8" (premise 8),
   add_style "premise9" (premise 9),
-  add_style "conclusion" (K Logic.strip_imp_concl)];
+  add_style "concl" (K Logic.strip_imp_concl)];
 
 end;