45 NONE => error "mstools: syntax error" |
45 NONE => error "mstools: syntax error" |
46 | SOME t' => t'; |
46 | SOME t' => t'; |
47 if ((lhs t) |> type_of) = @{typ int} then () |
47 if ((lhs t) |> type_of) = @{typ int} then () |
48 else error "mstools: incorrect type inference from parseNEW ctxt"; |
48 else error "mstools: incorrect type inference from parseNEW ctxt"; |
49 |
49 |
|
50 val t_bit = Syntax.read_term ctxt "11::int"; |
|
51 val t_free = numbers_to_string t_bit; |
|
52 val ctxt = ProofContext.init_global @{theory "Isac"}; |
|
53 val SOME t = parseNEW ctxt "11"; |
|
54 if (t |> type_of) = TFree ("'a", ["Int.number"]) then () |
|
55 else error "parsed numeral correct"; |
|
56 val ctxt' = Variable.declare_constraints t_free ctxt; |
|
57 val SOME t' = parseNEW ctxt' "11"; |
|
58 if (t' |> type_of) = TFree ("'a", ["Int.number"]) then () |
|
59 else error "Variable.declare_constraints did not recognize numeral"; |
50 |
60 |
51 "----------- fun get_assumptions, fun get_environments --"; |
61 "----------- fun get_assumptions, fun get_environments --"; |
52 "----------- fun get_assumptions, fun get_environments --"; |
62 "----------- fun get_assumptions, fun get_environments --"; |
53 "----------- fun get_assumptions, fun get_environments --"; |
63 "----------- fun get_assumptions, fun get_environments --"; |
54 val ctxt = insert_assumptions |
64 val ctxt = insert_assumptions |