1.1 --- a/src/Tools/isac/Interpret/script.sml	Fri Jul 26 16:34:41 2019 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Wed Jul 31 09:46:50 2019 +0200
     1.3 @@ -209,13 +209,10 @@
     1.4    | stac2tac_ _ _ (Const("Script.Or'_to'_List", _) $ _ ) = (Tactic.Or_to_List, Tactic.Empty_Tac_)
     1.5  
     1.6      (*compare "| associate _ (Subproblem'" ..TODO: extract common code *)
     1.7 -  | stac2tac_ pt _ (stac as Const ("Script.SubProblem", _) $
     1.8 -     (Const ("Product_Type.Pair", _) $ dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags') =
     1.9 +  | stac2tac_ pt _ (stac as Const ("Script.SubProblem", _) $ spec' $ ags') =
    1.10      let
    1.11 -      val dI = HOLogic.dest_string dI';
    1.12 +      val (dI, pI, mI) = LTool.dest_spec spec'
    1.13        val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
    1.14 -	    val pI = pI' |> HOLogic.dest_list |> map HOLogic.dest_string;
    1.15 -	    val mI = mI' |> HOLogic.dest_list |> map HOLogic.dest_string;
    1.16  	    val ags = TermC.isalist2list ags';
    1.17  	    val (pI, pors, mI) = 
    1.18  	      if mI = ["no_met"] 
    1.19 @@ -373,13 +370,10 @@
    1.20  
    1.21      (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)" ..TODO: extract common code *)
    1.22    | associate pt _ (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _))
    1.23 -      (stac as Const ("Script.SubProblem", _) $ (Const ("Product_Type.Pair", _) $ 
    1.24 -        dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags') =
    1.25 +      (stac as Const ("Script.SubProblem", _) $ spec' $ ags') =
    1.26      let
    1.27 -      val dI = HOLogic.dest_string dI';
    1.28 +      val (dI, pI, mI) = LTool.dest_spec spec'
    1.29        val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
    1.30 -	    val pI = pI' |> HOLogic.dest_list |> map HOLogic.dest_string;
    1.31 -	    val mI = mI' |> HOLogic.dest_list |> map HOLogic.dest_string;
    1.32  	    val ags = TermC.isalist2list ags';
    1.33  	    val (pI, pors, mI) = 
    1.34  	      if mI = ["no_met"]

     2.1 --- a/src/Tools/isac/ProgLang/scrtools.sml	Fri Jul 26 16:34:41 2019 +0200
     2.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml	Wed Jul 31 09:46:50 2019 +0200
     2.3 @@ -26,8 +26,9 @@
     2.4      val get_calcs: theory -> term -> (Rule.prog_calcID * (Rule.calID * Rule.eval_fn)) list
     2.5      val prep_rls: theory -> Rule.rls -> Rule.rls
     2.6      val prep_program : thm -> term
     2.7 -  val formal_args : term -> term list
     2.8 -  val body_of : term -> term
     2.9 +    val formal_args : term -> term list
    2.10 +    val body_of : term -> term
    2.11 +    val dest_spec : term -> Celem.spec
    2.12  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    2.13    (* NONE *)
    2.14  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    2.15 @@ -39,10 +40,14 @@
    2.16  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.17    end
    2.18  
    2.19 -(**)
    2.20  structure LTool(**): LANGUAGE_TOOLS(**) =
    2.21  struct
    2.22 -(**)
    2.23 +
    2.24 +fun dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) $ p $ m)) =
    2.25 +    (d |> HOLogic.dest_string, 
    2.26 +     p |> HOLogic.dest_list |> map HOLogic.dest_string,
    2.27 +     m |> HOLogic.dest_list |> map HOLogic.dest_string) : Celem.spec
    2.28 +  | dest_spec t = raise TERM ("dest_spec: called with ", [t])
    2.29  
    2.30  fun prep_program thm = (thm
    2.31    |> Thm.prop_of