signature SUB_PROBLEM =

 sig

   val tac_from_prog: Ctree.ctree -> term -> Tactic.input * Tactic.T

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

   (*NONE*)

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

   (*NONE*)

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 end

 (**)

 structure Sub_Problem(**): SUB_PROBLEM(**) =

 struct

 (**)

 fun tac_from_prog pt (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags') =

     let

       val (dI, pI, mI) = Prog_Tac.dest_spec spec'

       val thy = Stool.common_subthy (Celem.assoc_thy dI, Ctree.rootthy pt);

 	    val ags = TermC.isalist2list ags';

 	    val (pI, pors, mI) = 

 	      if mI = ["no_met"]

 	      then

           let

             val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)

             (*    Chead.match_ags : theory -> pat list                 -> term list -> ori list

                                               ^^^ variables               ^^^ values          *)

 		          handle ERROR "actual args do not match formal args"

 			          => (Chead.match_ags_msg pI stac ags (*raise exn*);[]);

 		        val pI' = Specify.refine_ori' pors pI;

 		      in (pI', pors (* refinement over models with diff.prec only *), 

 		          (hd o #met o Specify.get_pbt) pI') end

 	      else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)

 		      handle ERROR "actual args do not match formal args"

 		      => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);

       val (fmz_, vals) = Chead.oris2fmz_vals pors;

 	    val {cas, ppc, thy, ...} = Specify.get_pbt pI

 	    val dI = ThyC.theory2theory' thy (*take dI from _refined_ pbl*)

 	    val dI = ThyC.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, Ctree.rootthy pt))

 	    val ctxt = ContextC.initialise dI vals

 	    val hdl =

         case cas of

 		      NONE => Auto_Prog.pblterm dI pI

 		    | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t

       val f = Auto_Prog.subpbl (strip_thy dI) pI

     in

       (Tactic.Subproblem (dI, pI),	Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))

     end

   | tac_from_prog _ t = raise ERROR ("tac_from_prog not impl. for " ^ Rule.term2str t)

 (**)end(**)