test/Tools/isac/Minisubpbl/100-init-rootpbl.sml
branchdecompose-isar
changeset 42012 e0144cf528e1
parent 42011 6a9ba30ab6bc
child 42013 e9ef067fcf2a
     1.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml	Fri May 20 08:12:51 2011 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml	Fri May 20 08:17:46 2011 +0200
     1.3 @@ -10,8 +10,6 @@
     1.4  val (dI',pI',mI') =
     1.5    ("Test", ["sqroot-test","univariate","equation","test"],
     1.6     ["Test","squ-equ-test-subpbl1"]);
     1.7 -*}
     1.8 -ML {*
     1.9  "~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
    1.10  "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz : fmz_, (dI, pI, mI) : spec) = (fmz, sp);
    1.11  val thy = assoc_thy dI
    1.12 @@ -21,6 +19,7 @@
    1.13  val dI = theory2theory' (maxthy thy thy');
    1.14  val hdl =
    1.15    case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
    1.16 +            | _ => error "Minisubplb/100-init-rootpbl.sml no headline"
    1.17  val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
    1.18  				  (pors, (dI, pI, mI), hdl)
    1.19  val pt = update_ctxt pt [] pctxt