# HG changeset patch
# User aspinall
# Date 1169481146 -3600
# Node ID ac1bae165ad84c3bd5ee60067d6758422db914c8
# Parent  a586b0af857e09451428bd031f8c69c5368b0783
Test askref

diff -r a586b0af857e -r ac1bae165ad8 src/Pure/ProofGeneral/pgip_tests.ML
--- a/src/Pure/ProofGeneral/pgip_tests.ML	Mon Jan 22 16:52:02 2007 +0100
+++ b/src/Pure/ProofGeneral/pgip_tests.ML	Mon Jan 22 16:52:26 2007 +0100
@@ -68,6 +68,7 @@
 	      | _ => error("Expected to get an XML Element")
 
 open PgipInput;
+open PgipTypes;
 
 fun asseqi a b =
     if input (e a) = b then ()
@@ -82,6 +83,8 @@
 val _ = asseqi "<pgmlsymbolsoff/>" (SOME (Pgmlsymbolsoff()));
 val _ = asseqi "<startquiet/>" (SOME (Startquiet()));
 val _ = asseqi "<stopquiet/>" (SOME (Stopquiet()));
+val _ = asseqi "<askrefs thyname='foo' objtype='theory'/>" (SOME (Askrefs {url=NONE, thyname=SOME "foo",
+									  objtype=SOME ObjTheory,name=NONE}));
 val _ = asseqi "<otherelt/>" NONE;
 
 end