src/Tools/isac/Interpret/calchead.sml
branchdecompose-isar
changeset 42090 908dfde7cf75
parent 42011 6a9ba30ab6bc
child 42092 1a6d6089e594
     1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Fri Jul 15 10:17:51 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Fri Jul 15 13:51:50 2011 +0200
     1.3 @@ -1724,17 +1724,16 @@
     1.4     oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
     1.5  fun all_modspec (pt, (p,_):pos') =
     1.6    let 
     1.7 -    val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
     1.8 -		  ...}) = get_obj I pt p;
     1.9 +    val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
    1.10      val thy = assoc_thy dI;
    1.11 -	  val {ppc,...} = get_met mI;
    1.12 +	  val {ppc, ...} = get_met mI;
    1.13  	  val mors = prep_ori fmz_ thy ppc |> #1;
    1.14      val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
    1.15  	  val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
    1.16  	  val pt = update_spec pt p (dI,pI,mI);
    1.17    in (pt, (p,Met): pos') end;
    1.18  
    1.19 -(*WN.12.03: use in nxt_spec, too ? what about variants ???*)
    1.20 +(*WN0312: use in nxt_spec, too ? what about variants ???*)
    1.21  fun is_complete_mod_ ([]: itm list) = false
    1.22    | is_complete_mod_ itms = 
    1.23      foldl and_ (true, (map #3 itms));