1.1 --- a/src/Tools/eqsubst.ML	Fri Mar 13 21:24:21 2009 +0100
     1.2 +++ b/src/Tools/eqsubst.ML	Fri Mar 13 21:25:15 2009 +0100
     1.3 @@ -109,8 +109,8 @@
     1.4         searchinfo -> Term.term -> match Seq.seq Seq.seq
     1.5  
     1.6      (* syntax tools *)
     1.7 -    val ith_syntax : Args.T list -> int list * Args.T list
     1.8 -    val options_syntax : Args.T list -> bool * Args.T list
     1.9 +    val ith_syntax : int list parser
    1.10 +    val options_syntax : bool parser
    1.11  
    1.12      (* Isar level hooks *)
    1.13      val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method