1.1 --- a/src/Tools/isac/Interpret/script.sml	Mon Dec 31 14:49:16 2018 +0100
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu Jan 10 18:17:48 2019 +0100
     1.3 @@ -217,7 +217,8 @@
     1.4      val _ = if pats = [] then raise ERROR errmsg else ()
     1.5    in (flat o (map (itm2arg itms))) pats end;
     1.6  
     1.7 -(* convert a script-tac 'stac' to a tactic 'tac';
     1.8 +(* convert a script-tac 'stac' to 'tac' for users;
     1.9 +   for "Script.SubProblem" also create a 'tac_' for internal use. FIXME separate?
    1.10     if stac is an initac, then convert to a 'tac_' (as required in appy).
    1.11     arg ctree for pushing the thy specified in rootpbl into subpbls    *)
    1.12  fun stac2tac_ _ thy (Const ("Script.Rewrite", _) $ thmID $ _ $ _) =
    1.13 @@ -226,10 +227,8 @@
    1.14      in (Tac.Rewrite (tid, Rewrite.assoc_thm'' thy tid), Tac.Empty_Tac_) end
    1.15    | stac2tac_ _ thy (Const ("Script.Rewrite'_Inst", _) $ sub $ thmID $ _ $ _) =
    1.16      let
    1.17 -      val subML = ((map TermC.isapair2pair) o TermC.isalist2list) sub
    1.18 -      val subStr = Selem.subst2subs subML
    1.19 -      val tid = HOLogic.dest_string thmID (*4.10.02 unnoetig*)
    1.20 -    in (Tac.Rewrite_Inst (subStr, (tid, Rewrite.assoc_thm'' thy tid)), Tac.Empty_Tac_) end
    1.21 +      val tid = HOLogic.dest_string thmID
    1.22 +    in (Tac.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid)), Tac.Empty_Tac_) end
    1.23    | stac2tac_ _ _ (Const ("Script.Rewrite'_Set",_) $ rls $ _ $ _) =
    1.24       (Tac.Rewrite_Set (HOLogic.dest_string rls), Tac.Empty_Tac_)
    1.25    | stac2tac_ _ _ (Const ("Script.Rewrite'_Set'_Inst", _) $ sub $ rls $ _ $ _) =
    1.26 @@ -486,14 +485,14 @@
    1.27    let val ct = Thm.global_cterm_of thy (HOLogic.Trueprop $ t)
    1.28    in Rule.Thm (Rule.term_to_string''' thy (Thm.term_of ct), Thm.make_thm ct) end;
    1.29  
    1.30 -fun rep_tac_ (Tac.Rewrite_Inst' (thy', _, _, put, subs, (thmID, _), f, (f', _))) = 
    1.31 -    let val fT = type_of f;
    1.32 -      val b = if put then @{term True} else @{term False};
    1.33 -      val sT = (type_of o fst o hd) subs;
    1.34 -      val subs' = TermC.list2isalist (HOLogic.mk_prodT (sT, sT)) (map HOLogic.mk_prod subs);
    1.35 +fun rep_tac_ (Tac.Rewrite_Inst' (thy', _, _, _, subs, (thmID, _), f, (f', _))) = 
    1.36 +    let
    1.37 +      val b = @{term False};
    1.38 +      val subs' = Selem.subst_to_subst' subs;
    1.39        val sT' = type_of subs';
    1.40 +      val fT = type_of f;
    1.41        val lhs = Const ("Script.Rewrite'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT) 
    1.42 -        $ subs' $ Free (thmID, HOLogic.stringT) $ b $ f;
    1.43 +        $ subs' $ HOLogic.mk_string thmID $ b $ f;
    1.44      in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
    1.45    | rep_tac_ (Tac.Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
    1.46      let 
    1.47 @@ -502,7 +501,15 @@
    1.48        val lhs = Const ("Script.Rewrite", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
    1.49          $ HOLogic.mk_string thmID $ b $ f;
    1.50      in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
    1.51 -  | rep_tac_ (Tac.Rewrite_Set_Inst' (_, _, _, _, _, (f', _))) = (Rule.e_rule, (Rule.e_term, f'))
    1.52 +  | rep_tac_ (Tac.Rewrite_Set_Inst' (thy', _, subs, rls, f, (f', _))) =
    1.53 +    let
    1.54 +      val b = @{term False};
    1.55 +      val subs' = Selem.subst_to_subst' subs;
    1.56 +      val sT' = type_of subs';
    1.57 +      val fT = type_of f;
    1.58 +      val lhs = Const ("Script.Rewrite'_Set'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT) 
    1.59 +        $ subs' $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
    1.60 +    in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
    1.61    | rep_tac_ (Tac.Rewrite_Set' (thy', put, rls, f, (f', _))) =
    1.62      let 
    1.63        val fT = type_of f;
    1.64 @@ -924,14 +931,14 @@
    1.65  	    (_, LTool.Expr s) => Skip (s, E)
    1.66      | (a', LTool.STac stac) =>
    1.67  	    let val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac
    1.68 -      in case m of 
    1.69 +      in case m of
    1.70  	      Tac.Subproblem _ => Appy (m', (E,l,a',tac_2res m',Selem.Sundef,false))
    1.71  	    | _ =>
    1.72          (case Applicable.applicable_in p pt m of
    1.73  		       Chead.Appl m' => (Appy (m', (E,l,a',tac_2res m',Selem.Sundef,false)))
    1.74  		     | _ => Napp E)
    1.75  	    end
    1.76 -(*GOON*)
    1.77 +
    1.78  fun nxt_up thy ptp (scr as (Rule.Prog sc)) E l ay (Const ("HOL.Let", _) $ _) a v = (*comes from let=...*)
    1.79      if ay = Napp_
    1.80      then nstep_up thy ptp scr E (drop_last l) Napp_ a v