1.1 --- a/src/Tools/isac/Interpret/appl.sml	Thu Oct 24 14:08:32 2013 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Thu Oct 24 15:00:44 2013 +0200
     1.3 @@ -17,52 +17,47 @@
     1.4  
     1.5  (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
     1.6  fun from_pblobj_or_detail_thm thm' p pt = 
     1.7 -    let val (pbl,p',rls') = par_pbl_det pt p
     1.8 -    in if pbl
     1.9 -       then let (*val _= tracing("### from_pblobj_or_detail_thm: pbl=true")*)
    1.10 -	        val thy' = get_obj g_domID pt p'
    1.11 -		val {rew_ord',erls,(*asm_thm,*)...} = 
    1.12 -		    get_met (get_obj g_metID pt p')
    1.13 -		(*val _= tracing("### from_pblobj_or_detail_thm: metID= "^
    1.14 -			       (metID2str(get_obj g_metID pt p')))
    1.15 -		val _= tracing("### from_pblobj_or_detail_thm: erls= "^erls)*)
    1.16 -	    in ("OK",thy',rew_ord',erls,(*put_asm*)false) 
    1.17 -	    end
    1.18 -       else ((*tracing("### from_pblobj_or_detail_thm: pbl=false");*)
    1.19 -	     (*case assoc(!ruleset', rls') of  !!!FIXME.3.4.03:re-organize !!!
    1.20 -		NONE => ("unknown ruleset '"^rls'^"'","","",Erls,false)
    1.21 -	      | SOME rls =>*)
    1.22 -		let val thy' = get_obj g_domID pt (par_pblobj pt p)
    1.23 -		    val (rew_ord',erls,(*asm_thm,*)_) = rew_info rls'
    1.24 -		in ("OK",thy',rew_ord',erls,false) end)
    1.25 -    end;
    1.26 +  let 
    1.27 +    val (pbl, p', rls') = par_pbl_det pt p
    1.28 +  in 
    1.29 +    if pbl
    1.30 +    then 
    1.31 +      let 
    1.32 +        val thy' = get_obj g_domID pt p'
    1.33 +        val {rew_ord', erls, ...} = et_met (get_obj g_metID pt p')              
    1.34 +	    in ("OK", thy', rew_ord', erls, false) end
    1.35 +     else 
    1.36 +      let
    1.37 +        val thy' = get_obj g_domID pt (par_pblobj pt p)
    1.38 +		    val (rew_ord', erls, _) = rew_info rls'
    1.39 +		  in ("OK",thy',rew_ord',erls,false) end
    1.40 +  end;
    1.41  (*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*)
    1.42  fun from_pblobj_or_detail_calc scrop p pt = 
    1.43 -(* val (scrop, p, pt) = (op_, p, pt);
    1.44 -   *)
    1.45 -    let val (pbl,p',rls') = par_pbl_det pt p
    1.46 -    in if pbl
    1.47 -       then let val thy' = get_obj g_domID pt p'
    1.48 -		val {calc = scr_isa_fns,...} = 
    1.49 -		    get_met (get_obj g_metID pt p')
    1.50 -		val opt = assoc (scr_isa_fns, scrop)
    1.51 -	    in case opt of
    1.52 -		   SOME isa_fn => ("OK",thy',isa_fn)
    1.53 -		 | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
    1.54 -			    "",("",e_evalfn)) end
    1.55 -       else (*case assoc(!ruleset', rls') of
    1.56 -		NONE => ("unknown ruleset '"^rls'^"'","",("",e_evalfn))
    1.57 -	      | SOME rls => !!!FIXME.3.4.03:re-organize from_pblobj_or_detai*)
    1.58 -		(* val SOME rls = assoc(!ruleset', rls');
    1.59 -		   *)
    1.60 -		let val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.61 +  let
    1.62 +    val (pbl,p',rls') = par_pbl_det pt p
    1.63 +  in
    1.64 +    if pbl
    1.65 +    then
    1.66 +      let
    1.67 +        val thy' = get_obj g_domID pt p'
    1.68 +        val {calc = scr_isa_fns,...} = get_met (get_obj g_metID pt p')
    1.69 +        val opt = assoc (scr_isa_fns, scrop)
    1.70 +	    in
    1.71 +	      case opt of
    1.72 +	        SOME isa_fn => ("OK",thy',isa_fn)
    1.73 +	      | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", e_evalfn))
    1.74 +	    end
    1.75 +    else 
    1.76 +		  let
    1.77 +		    val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.78  		    val (_,_,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
    1.79 -		in case assoc (scr_isa_fns, scrop) of
    1.80 -		   SOME isa_fn => ("OK",thy',isa_fn)
    1.81 -		 | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
    1.82 -			    "",("",e_evalfn)) end
    1.83 -    end;
    1.84 -(*------------------------------------------------------------------*)
    1.85 +		  in
    1.86 +		    case assoc (scr_isa_fns, scrop) of
    1.87 +		      SOME isa_fn => ("OK",thy',isa_fn)
    1.88 +		    | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", e_evalfn))
    1.89 +		  end
    1.90 +  end;
    1.91  
    1.92  val op_and = Const ("op &", [bool, bool] ---> bool);
    1.93  (*> (cterm_of thy) (op_and $ Free("a",bool) $ Free("b",bool));