src/Pure/Thy/term_style.ML
changeset 32891 d403b99287ff
parent 32890 77df12652210
child 33184 de8cc01e8d9e
     1.1 --- a/src/Pure/Thy/term_style.ML	Wed Oct 07 16:57:56 2009 +0200
     1.2 +++ b/src/Pure/Thy/term_style.ML	Thu Oct 08 15:16:13 2009 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4  
     1.5  (* predefined styles *)
     1.6  
     1.7 -fun style_binargs proj = Scan.succeed (fn ctxt => fn t =>
     1.8 +fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
     1.9    let
    1.10      val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
    1.11        (Logic.strip_imp_concl t)
    1.12 @@ -71,16 +71,31 @@
    1.13      | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
    1.14    end);
    1.15  
    1.16 +val style_prem = Args.name >> (fn raw_i => fn ctxt => fn t =>
    1.17 +  let
    1.18 +    val i = (the o Int.fromString) raw_i;
    1.19 +    val prems = Logic.strip_imp_prems t;
    1.20 +  in
    1.21 +    if i <= length prems then nth prems (i - 1)
    1.22 +    else error ("Not enough premises for prem " ^ string_of_int i ^
    1.23 +      " in propositon: " ^ Syntax.string_of_term ctxt t)
    1.24 +  end);
    1.25 +
    1.26  fun style_parm_premise i = Scan.succeed (fn ctxt => fn t =>
    1.27 -  let val prems = Logic.strip_imp_prems t in
    1.28 +  let
    1.29 +    val i_str = string_of_int i;
    1.30 +    val prems = Logic.strip_imp_prems t;
    1.31 +  in
    1.32      if i <= length prems then nth prems (i - 1)
    1.33      else error ("Not enough premises for prem" ^ string_of_int i ^
    1.34        " in propositon: " ^ Syntax.string_of_term ctxt t)
    1.35    end);
    1.36  
    1.37  val _ = Context.>> (Context.map_theory
    1.38 - (setup "lhs" (style_binargs fst) #>
    1.39 -  setup "rhs" (style_binargs snd) #>
    1.40 + (setup "lhs" (style_lhs_rhs fst) #>
    1.41 +  setup "rhs" (style_lhs_rhs snd) #>
    1.42 +  setup "prem" style_prem #>
    1.43 +  setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
    1.44    setup "prem1" (style_parm_premise 1) #>
    1.45    setup "prem2" (style_parm_premise 2) #>
    1.46    setup "prem3" (style_parm_premise 3) #>
    1.47 @@ -99,7 +114,6 @@
    1.48    setup "prem16" (style_parm_premise 16) #>
    1.49    setup "prem17" (style_parm_premise 17) #>
    1.50    setup "prem18" (style_parm_premise 18) #>
    1.51 -  setup "prem19" (style_parm_premise 19) #>
    1.52 -  setup "concl" (Scan.succeed (K Logic.strip_imp_concl))));
    1.53 +  setup "prem19" (style_parm_premise 19)));
    1.54  
    1.55  end;