diff -r 6a9ba30ab6bc -r e0144cf528e1 test/Tools/isac/Minisubpbl/100-init-rootpbl.sml --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Fri May 20 08:12:51 2011 +0200 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Fri May 20 08:17:46 2011 +0200 @@ -10,8 +10,6 @@ val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"], ["Test","squ-equ-test-subpbl1"]); -*} -ML {* "~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))]; "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz : fmz_, (dI, pI, mI) : spec) = (fmz, sp); val thy = assoc_thy dI @@ -21,6 +19,7 @@ val dI = theory2theory' (maxthy thy thy'); val hdl = case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t; + | _ => error "Minisubplb/100-init-rootpbl.sml no headline" val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl) val pt = update_ctxt pt [] pctxt