1.1 --- a/test/Tools/isac/Interpret/mstools.sml	Tue Sep 13 10:51:56 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/mstools.sml	Sun Sep 18 15:21:46 2011 +0200
     1.3 @@ -47,6 +47,16 @@
     1.4  if ((lhs t) |> type_of) = @{typ int} then ()
     1.5    else error "mstools: incorrect type inference from parseNEW ctxt";
     1.6  
     1.7 +val t_bit = Syntax.read_term ctxt "11::int";
     1.8 +val t_free = numbers_to_string t_bit;
     1.9 +val ctxt = ProofContext.init_global @{theory "Isac"};
    1.10 +val SOME t = parseNEW ctxt "11";
    1.11 +if (t |> type_of) = TFree ("'a", ["Int.number"]) then ()
    1.12 +else error "parsed numeral correct";
    1.13 +val ctxt' = Variable.declare_constraints t_free ctxt;
    1.14 +val SOME t' = parseNEW ctxt' "11";
    1.15 +if (t' |> type_of) = TFree ("'a", ["Int.number"]) then ()
    1.16 +else error "Variable.declare_constraints did not recognize numeral";
    1.17  
    1.18  "----------- fun get_assumptions, fun get_environments --";
    1.19  "----------- fun get_assumptions, fun get_environments --";