changeset 23834 | ad6ad61332fa |
parent 23749 | ac6d3a8d22b5 |
child 26548 | 41bbcaf3e481 |
--- a/src/Pure/ProofGeneral/pgip_output.ML Tue Jul 17 16:06:13 2007 +0200 +++ b/src/Pure/ProofGeneral/pgip_output.ML Tue Jul 17 16:14:42 2007 +0200 @@ -350,7 +350,7 @@ content) end -fun ready (Ready vs) = XML.Elem("ready",[],[]) +fun ready (Ready _) = XML.Elem("ready",[],[]) fun output pgipoutput = case pgipoutput of