src/Pure/ProofGeneral/pgip_input.ML
changeset 38228 ada3ab6b9085
parent 36692 54b64d4ad524
     1.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Sat Aug 07 19:52:14 2010 +0200
     1.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Sat Aug 07 21:03:06 2010 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4      (* unofficial escape command for debugging *)
     1.5      | Quitpgip       of { }
     1.6  
     1.7 -    val input: string * XML.attributes * XML.tree list -> pgipinput option  (* raises PGIP *)
     1.8 +    val input: Markup.T * XML.tree list -> pgipinput option  (* raises PGIP *)
     1.9  end
    1.10  
    1.11  structure PgipInput : PGIPINPUT = 
    1.12 @@ -161,7 +161,7 @@
    1.13     Raise PGIP exception for invalid data.
    1.14     Return NONE for unknown/unhandled commands. 
    1.15  *)
    1.16 -fun input (elem, attrs, data) =
    1.17 +fun input ((elem, attrs), data) =
    1.18  SOME 
    1.19   (case elem of 
    1.20       "askpgip"        => Askpgip { }