--- 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;