# HG changeset patch
# User haftmann
# Date 1117615937 -7200
# Node ID b2e4c4058b7110c808a54c0f6ad6b42659585462
# Parent  346bb10d4bbbc48c3dac268b07753ac5f53ee5eb
renamed premise* to prem

diff -r 346bb10d4bbb -r b2e4c4058b71 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Jun 01 10:40:51 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Jun 01 10:52:17 2005 +0200
@@ -212,17 +212,17 @@
 own way, you can extract the premises and the conclusion explicitly
 and combine them as you like:
 \begin{itemize}
-\item \verb!@!\verb!{thm_style premise1! $thm$\verb!}!
-prints premise 1 of $thm$ (and similarly up to \texttt{premise9}).
+\item \verb!@!\verb!{thm_style prem1! $thm$\verb!}!
+prints premise 1 of $thm$ (and similarly up to \texttt{prem9}).
 \item \verb!@!\verb!{thm_style concl! $thm$\verb!}!
 prints the conclusion of $thm$.
 \end{itemize}
-For example, ``from @{thm_style premise2 conjI} and
-@{thm_style premise1 conjI} we conclude @{thm_style concl conjI}''
+For example, ``from @{thm_style prem2 conjI} and
+@{thm_style prem1 conjI} we conclude @{thm_style concl conjI}''
 is produced by
 \begin{quote}
-\verb!from !\verb!@!\verb!{thm_style premise2 conjI}!\\
-\verb!and !\verb!@!\verb!{thm_style premise1 conjI}!\\
+\verb!from !\verb!@!\verb!{thm_style prem2 conjI}!\\
+\verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\
 \verb!we conclude !\verb!@!\verb!{thm_style concl conjI}!
 \end{quote}
 Thus you can rearrange or hide premises and typeset the theorem as you like.
@@ -324,7 +324,7 @@
     \end{quote}
 
   A ``style'' is a transformation of propositions. There are predefined
-  styles, namly \verb!lhs! and \verb!rhs!, \verb!premise1! unto \verb!premise9!, and \verb!concl!.
+  styles, namly \verb!lhs! and \verb!rhs!, \verb!prem1! up to \verb!prem9!, and \verb!concl!.
   For example, 
   the output
   \begin{center}
diff -r 346bb10d4bbb -r b2e4c4058b71 src/Pure/Isar/term_style.ML
--- a/src/Pure/Isar/term_style.ML	Wed Jun 01 10:40:51 2005 +0200
+++ b/src/Pure/Isar/term_style.ML	Wed Jun 01 10:52:17 2005 +0200
@@ -57,24 +57,25 @@
     | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
   end;
 
-fun premise i _ t =
+fun style_parm_premise i ctxt t =
   let val prems = Logic.strip_imp_prems t
   in if i <= length prems then List.nth(prems, i-1)
-     else error ("Not enough premises: premise" ^ string_of_int i)
+     else error ("Not enough premises for prem" ^ string_of_int i ^
+                 " in propositon: " ^ ProofContext.string_of_term ctxt t)
   end;
- 
+
 val _ = Context.add_setup
  [add_style "lhs" (fst oo style_binargs),
   add_style "rhs" (snd oo style_binargs),
-  add_style "premise1" (premise 1),
-  add_style "premise2" (premise 2),
-  add_style "premise3" (premise 3),
-  add_style "premise4" (premise 4),
-  add_style "premise5" (premise 5),
-  add_style "premise6" (premise 6),
-  add_style "premise7" (premise 7),
-  add_style "premise8" (premise 8),
-  add_style "premise9" (premise 9),
+  add_style "prem1" (style_parm_premise 1),
+  add_style "prem2" (style_parm_premise 2),
+  add_style "prem3" (style_parm_premise 3),
+  add_style "prem4" (style_parm_premise 4),
+  add_style "prem5" (style_parm_premise 5),
+  add_style "prem6" (style_parm_premise 6),
+  add_style "prem7" (style_parm_premise 7),
+  add_style "prem8" (style_parm_premise 8),
+  add_style "prem9" (style_parm_premise 9),
   add_style "concl" (K Logic.strip_imp_concl)];
 
 end;