1.1 --- a/test/Tools/isac/Interpret/ctree.sml	Fri May 13 11:45:07 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Fri May 13 14:15:59 2011 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4  "table of contents -----------------------------------------------";
     1.5  "-----------------------------------------------------------------";
     1.6  "-----------------------------------------------------------------";
     1.7 +"-------------- fun update_ctxt, fun g_ctxt ----------------------";
     1.8  "-------------- check positions in miniscript --------------------";
     1.9  "-------------- get_allpos' (from ptree above)--------------------";
    1.10  (**#####################################################################(**)
    1.11 @@ -58,6 +59,18 @@
    1.12  "-----------------------------------------------------------------";
    1.13  
    1.14  
    1.15 +"-------------- fun update_ctxt, fun g_ctxt ----------------------";
    1.16 +"-------------- fun update_ctxt, fun g_ctxt ----------------------";
    1.17 +"-------------- fun update_ctxt, fun g_ctxt ----------------------";
    1.18 +val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) EmptyPtree;
    1.19 +if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name)
    1.20 +    = "Interpret"
    1.21 +then () else error "TODO";
    1.22 +val pt = update_ctxt pt [] (ProofContext.init_global @{theory "Isac"});
    1.23 +if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name)
    1.24 +    = "Isac"
    1.25 +then () else error "TODO";
    1.26 +
    1.27  "-------------- check positions in miniscript --------------------";
    1.28  "-------------- check positions in miniscript --------------------";
    1.29  "-------------- check positions in miniscript --------------------";