1.1 --- a/src/Tools/isac/Interpret/script.sml	Wed May 11 16:51:30 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu May 12 08:26:02 2011 +0200
     1.3 @@ -367,75 +367,49 @@
     1.4     then convert to a 'tac_' (as required in appy).
     1.5     arg pt:ptree for pushing the thy specified in rootpbl into subpbls.*)
     1.6  fun stac2tac_ pt thy (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ f) =
     1.7 -(* val (pt, thy, (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ f)) = 
     1.8 -       (pt, (assoc_thy th), stac);
     1.9 -   *)
    1.10 -    let val tid = (de_esc_underscore o strip_thy) thmID
    1.11 -    in (Rewrite (tid, (string_of_thmI o 
    1.12 -		       (assoc_thm' thy)) (tid,"")), Empty_Tac_) end
    1.13 -(* val (thy,
    1.14 -	mm as(Const ("Script.Rewrite'_Inst",_) $  sub $ Free(thmID,_) $ _ $ f))
    1.15 -     = (assoc_thy th,stac);
    1.16 -   stac2tac_ pt thy mm;
    1.17 +      let
    1.18 +        val tid = (de_esc_underscore o strip_thy) thmID
    1.19 +      in (Rewrite (tid, (string_of_thmI o (assoc_thm' thy)) (tid,"")), Empty_Tac_)
    1.20 +      end
    1.21  
    1.22 -   assoc_thm' (assoc_thy "Isac") (tid,"");
    1.23 -   assoc_thm' (Thy_Info.get_theory "Isac") (tid,"");
    1.24 -   *)
    1.25 -  | stac2tac_ pt thy (Const ("Script.Rewrite'_Inst",_) $ 
    1.26 -	       sub $ Free (thmID,_) $ _ $ f) =
    1.27 -  let val subML = ((map isapair2pair) o isalist2list) sub
    1.28 -    val subStr = subst2subs subML
    1.29 -    val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)
    1.30 -  in (Rewrite_Inst 
    1.31 -	  (subStr, (tid, (string_of_thmI o
    1.32 -			  (assoc_thm' thy)) (tid,""))), Empty_Tac_) end
    1.33 +  | stac2tac_ pt thy (Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thmID,_) $ _ $ f) =
    1.34 +      let
    1.35 +        val subML = ((map isapair2pair) o isalist2list) sub
    1.36 +        val subStr = subst2subs subML
    1.37 +        val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)
    1.38 +      in (Rewrite_Inst (subStr, (tid, (string_of_thmI o (assoc_thm' thy)) (tid,""))), Empty_Tac_)
    1.39 +      end
    1.40        
    1.41 -  | stac2tac_ pt thy (Const ("Script.Rewrite'_Set",_) $ Free (rls,_) $ _ $ f)=
    1.42 -  (Rewrite_Set ((de_esc_underscore o strip_thy) rls), Empty_Tac_)
    1.43 +  | stac2tac_ pt thy (Const ("Script.Rewrite'_Set",_) $ Free (rls,_) $ _ $ f) =
    1.44 +      (Rewrite_Set ((de_esc_underscore o strip_thy) rls), Empty_Tac_)
    1.45  
    1.46 -  | stac2tac_ pt thy (Const ("Script.Rewrite'_Set'_Inst",_) $ 
    1.47 -	       sub $ Free (rls,_) $ _ $ f) =
    1.48 -  let val subML = ((map isapair2pair) o isalist2list) sub;
    1.49 -    val subStr = subst2subs subML;
    1.50 -  in (Rewrite_Set_Inst (subStr,rls), Empty_Tac_) end
    1.51 +  | stac2tac_ pt thy (Const ("Script.Rewrite'_Set'_Inst",_) $ sub $ Free (rls,_) $ _ $ f) =
    1.52 +      let
    1.53 +        val subML = ((map isapair2pair) o isalist2list) sub;
    1.54 +        val subStr = subst2subs subML;
    1.55 +      in (Rewrite_Set_Inst (subStr,rls), Empty_Tac_) end
    1.56  
    1.57    | stac2tac_ pt thy (Const ("Script.Calculate",_) $ Free (op_,_) $ f) =
    1.58 -  (Calculate op_, Empty_Tac_)
    1.59 +      (Calculate op_, Empty_Tac_)
    1.60  
    1.61    | stac2tac_ pt thy (Const ("Script.Take",_) $ t) =
    1.62 -  (Take (term2str t), Empty_Tac_)
    1.63 +      (Take (term2str t), Empty_Tac_)
    1.64  
    1.65    | stac2tac_ pt thy (Const ("Script.Substitute",_) $ isasub $ arg) =
    1.66 -  (Substitute ((subte2sube o isalist2list) isasub), Empty_Tac_)
    1.67 -(* val t = str2term"Substitute [x = L, M_b L = 0] (M_b x = q_0 * x + c)";
    1.68 -   val Const ("Script.Substitute", _) $ isasub $ arg = t;
    1.69 -   *)
    1.70 +      (Substitute ((subte2sube o isalist2list) isasub), Empty_Tac_)
    1.71  
    1.72 -(*12.1.01.*)
    1.73    | stac2tac_ pt thy (Const("Script.Check'_elementwise",_) $ _ $ 
    1.74 -		           (set as Const ("Collect",_) $ Abs (_,_,pred))) = 
    1.75 -    (Check_elementwise (Print_Mode.setmp [] (Syntax.string_of_term 
    1.76 -                                                 (thy2ctxt thy)) pred), 
    1.77 -   (*set*)Empty_Tac_)
    1.78 +		(set as Const ("Collect",_) $ Abs (_,_,pred))) = 
    1.79 +      (Check_elementwise (Print_Mode.setmp [] (Syntax.string_of_term 
    1.80 +                          (thy2ctxt thy)) pred), (*set*)Empty_Tac_)
    1.81  
    1.82    | stac2tac_ pt thy (Const("Script.Or'_to'_List",_) $ _ ) = 
    1.83 -  (Or_to_List, Empty_Tac_)
    1.84 +      (Or_to_List, Empty_Tac_)
    1.85  
    1.86 -(*12.1.01.for subproblem_equation_dummy in root-equation *)
    1.87 +    (*12.1.01.for subproblem_equation_dummy in root-equation *)
    1.88    | stac2tac_ pt thy (Const ("Script.Tac",_) $ Free (str,_)) = 
    1.89 -  (Tac ((de_esc_underscore o strip_thy) str),  Empty_Tac_) 
    1.90 -		    (*L_ will come from pt in appl_in*)
    1.91 +      (Tac ((de_esc_underscore o strip_thy) str),  Empty_Tac_) 
    1.92  
    1.93 -  (*3.12.03 copied from assod SubProblem*)
    1.94 -(* val Const ("Script.SubProblem",_) $
    1.95 -			 (Const ("Product_Type.Pair",_) $
    1.96 -				Free (dI',_) $ 
    1.97 -				(Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
    1.98 -    str2term 
    1.99 -    "SubProblem (EqSystem_, [linear, system], [no_met])\
   1.100 -    \            [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\
   1.101 -    \             REAL_LIST [c, c_2]]";
   1.102 -*)
   1.103    | stac2tac_ pt thy (stac as Const ("Script.SubProblem",_) $
   1.104  	  (Const ("Product_Type.Pair",_) $Free (dI',_) $ 
   1.105  		 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =