changeset 30513 | 1796b8ea88aa |
parent 30510 | 4120fc59dd85 |
child 31301 | 952d2d0c4446 |
--- a/src/Tools/eqsubst.ML Fri Mar 13 21:24:21 2009 +0100 +++ b/src/Tools/eqsubst.ML Fri Mar 13 21:25:15 2009 +0100 @@ -109,8 +109,8 @@ searchinfo -> Term.term -> match Seq.seq Seq.seq (* syntax tools *) - val ith_syntax : Args.T list -> int list * Args.T list - val options_syntax : Args.T list -> bool * Args.T list + val ith_syntax : int list parser + val options_syntax : bool parser (* Isar level hooks *) val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method