src/Pure/Isar/term_style.ML
changeset 16167 b2e4c4058b71
parent 16165 dbe9ee8ffcdd
child 16424 18a07ad8fea8
     1.1 --- a/src/Pure/Isar/term_style.ML	Wed Jun 01 10:40:51 2005 +0200
     1.2 +++ b/src/Pure/Isar/term_style.ML	Wed Jun 01 10:52:17 2005 +0200
     1.3 @@ -57,24 +57,25 @@
     1.4      | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
     1.5    end;
     1.6  
     1.7 -fun premise i _ t =
     1.8 +fun style_parm_premise i ctxt t =
     1.9    let val prems = Logic.strip_imp_prems t
    1.10    in if i <= length prems then List.nth(prems, i-1)
    1.11 -     else error ("Not enough premises: premise" ^ string_of_int i)
    1.12 +     else error ("Not enough premises for prem" ^ string_of_int i ^
    1.13 +                 " in propositon: " ^ ProofContext.string_of_term ctxt t)
    1.14    end;
    1.15 - 
    1.16 +
    1.17  val _ = Context.add_setup
    1.18   [add_style "lhs" (fst oo style_binargs),
    1.19    add_style "rhs" (snd oo style_binargs),
    1.20 -  add_style "premise1" (premise 1),
    1.21 -  add_style "premise2" (premise 2),
    1.22 -  add_style "premise3" (premise 3),
    1.23 -  add_style "premise4" (premise 4),
    1.24 -  add_style "premise5" (premise 5),
    1.25 -  add_style "premise6" (premise 6),
    1.26 -  add_style "premise7" (premise 7),
    1.27 -  add_style "premise8" (premise 8),
    1.28 -  add_style "premise9" (premise 9),
    1.29 +  add_style "prem1" (style_parm_premise 1),
    1.30 +  add_style "prem2" (style_parm_premise 2),
    1.31 +  add_style "prem3" (style_parm_premise 3),
    1.32 +  add_style "prem4" (style_parm_premise 4),
    1.33 +  add_style "prem5" (style_parm_premise 5),
    1.34 +  add_style "prem6" (style_parm_premise 6),
    1.35 +  add_style "prem7" (style_parm_premise 7),
    1.36 +  add_style "prem8" (style_parm_premise 8),
    1.37 +  add_style "prem9" (style_parm_premise 9),
    1.38    add_style "concl" (K Logic.strip_imp_concl)];
    1.39  
    1.40  end;