1.1 --- a/test/Tools/isac/Interpret/ctree.sml	Sun May 15 10:25:42 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Sun May 15 11:32:41 2011 +0200
     1.3 @@ -69,22 +69,21 @@
     1.4     ["Test","squ-equ-test-subpbl1"]);
     1.5  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
     1.6  (get_ctxt pt p)
     1.7 -  handle _ => error "ctree.sml: not even some ctxt found in PblObj";
     1.8 +  handle _ => error "--- fun get_ctxt not even some ctxt found in PblObj";
     1.9  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.10  (get_ctxt pt p)
    1.11 -  handle _ => error "ctree.sml: not even some ctxt found in PrfObj";
    1.12 +  handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";
    1.13  
    1.14  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
    1.15  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
    1.16  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
    1.17 -val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) EmptyPtree;
    1.18 -if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name)
    1.19 -    = "Interpret"
    1.20 -then () else error "TODO";
    1.21 +val pt = EmptyPtree;
    1.22 +val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) pt;
    1.23 +val ctxt = get_obj g_ctxt pt [];
    1.24 +if is_e_ctxt ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
    1.25  val pt = update_ctxt pt [] (ProofContext.init_global @{theory "Isac"});
    1.26 -if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name)
    1.27 -    = "Isac"
    1.28 -then () else error "TODO";
    1.29 +if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name) = "Isac"
    1.30 +then () else error "--- fun update_ctxt, fun g_ctxt changed";
    1.31  
    1.32  "-------------- check positions in miniscript --------------------";
    1.33  "-------------- check positions in miniscript --------------------";
    1.34 @@ -1337,3 +1336,4 @@
    1.35  *)
    1.36  
    1.37  ===== inhibit exn ?===========================================================*)
    1.38 +