clarified Simplifier diagnostics -- simplified ML;
unconditional warning for structural mistakes (NB: context of running Simplifier is not visible, and cond_warning ineffective);
theory ToyList_Test
imports Datatype
begin
ML {* (* FIXME somewhat non-standard, fragile *)
let
val texts =
map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode)
["ToyList1", "ToyList2"];
val trs = Outer_Syntax.parse Position.start (implode texts);
val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel;
in @{assert} (Toplevel.is_toplevel end_state) end;
*}
end