1.1 --- a/test/Tools/isac/Interpret/mstools.sml	Sat Mar 19 15:03:36 2011 +0100
     1.2 +++ b/test/Tools/isac/Interpret/mstools.sml	Sat Mar 19 15:09:19 2011 +0100
     1.3 @@ -8,13 +8,21 @@
     1.4  "--------------------------------------------------------";
     1.5  "table of contents --------------------------------------";
     1.6  "--------------------------------------------------------";
     1.7 -"----------- fun ----------------------------------------";
     1.8 +"----------- fun declare_constraints --------------------";
     1.9  "--------------------------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11  "--------------------------------------------------------";
    1.12 -"-----------------------------------------------------------------";
    1.13 +"--------------------------------------------------------";
    1.14  
    1.15  
    1.16 +"----------- fun declare_constraints --------------------";
    1.17 +"----------- fun declare_constraints --------------------";
    1.18 +"----------- fun declare_constraints --------------------";
    1.19 +val ctxt = ProofContext.init_global @{theory}
    1.20 +      |> declare_constraints "xxx + yyy = (111::int)";
    1.21 +val t = parseNEW ctxt "xxx = 123";
    1.22 +if ((rhs t) |> type_of) = @{typ int} then ()
    1.23 +  else error "mstools: incorrect type inference from parseNEW ctxt";
    1.24  
    1.25  (*========== inhibit exn =======================================================
    1.26  ============ inhibit exn =====================================================*)