src/Tools/isac/Interpret/calchead.sml
branchdecompose-isar
changeset 41977 a3ce4017f41d
parent 41976 792c59bf54d4
child 41980 6ec461ac6c76
     1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Thu May 05 14:21:54 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Fri May 06 11:18:07 2011 +0200
     1.3 @@ -1094,9 +1094,10 @@
     1.4      val (oris, ctxt) = 
     1.5        if dI' = e_domID orelse pI' = e_pblID 
     1.6        then ([], e_ctxt)
     1.7 -	    else pI' |> #ppc o get_pbt |> prep_ori fmz thy;
     1.8 +	    else pI' |> #ppc o get_pbt |> prep_ori fmz thy
     1.9      val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
    1.10 -			(oris, (dI',pI',mI'),e_term);
    1.11 +			(oris, (dI',pI',mI'),e_term)
    1.12 +      (*val pt = update_env pt [] (SOME (e_istate, ctxt))  GOON.WN110506*)
    1.13      val {ppc, prls, where_, ...} = get_pbt pI'
    1.14      val (pbl, pre, pb) = ([], [], false)
    1.15    in 
    1.16 @@ -1576,6 +1577,7 @@
    1.17  		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
    1.18          val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
    1.19  				  (pors, (dI, pI, mI), hdl)
    1.20 +          (* val pt = update_env pt [] (SOME (e_istate, pctxt))  GOON.WN110506*)
    1.21        in ((pt, ([], Pbl)), 
    1.22          fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
    1.23        end;