test/Tools/isac/Minisubpbl/100-init-rootpbl.sml
branchdecompose-isar
changeset 42013 e9ef067fcf2a
parent 42012 e0144cf528e1
child 59279 255c853ea2f0
     1.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml	Fri May 20 08:17:46 2011 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml	Fri May 20 08:20:53 2011 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  val {cas, ppc, thy=thy',...} = get_pbt pI
     1.5  val dI = theory2theory' (maxthy thy thy');
     1.6  val hdl =
     1.7 -  case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
     1.8 +  case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
     1.9              | _ => error "Minisubplb/100-init-rootpbl.sml no headline"
    1.10  val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
    1.11  				  (pors, (dI, pI, mI), hdl)