equal
deleted
inserted
replaced
63 (case concl of |
63 (case concl of |
64 (_ $ l $ r) => proj (l, r) |
64 (_ $ l $ r) => proj (l, r) |
65 | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)) |
65 | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)) |
66 end); |
66 end); |
67 |
67 |
68 val style_prem = Args.name >> (fn raw_i => fn ctxt => fn t => |
68 val style_prem = Parse.nat >> (fn i => fn ctxt => fn t => |
69 let |
69 let |
70 val i = (the o Int.fromString) raw_i; |
|
71 val prems = Logic.strip_imp_prems t; |
70 val prems = Logic.strip_imp_prems t; |
72 in |
71 in |
73 if i <= length prems then nth prems (i - 1) |
72 if i <= length prems then nth prems (i - 1) |
74 else |
73 else |
75 error ("Not enough premises for prem " ^ string_of_int i ^ |
74 error ("Not enough premises for prem " ^ string_of_int i ^ |