1.1 --- a/src/Tools/isac/Interpret/script.sml	Sun Jul 21 15:15:50 2013 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Mon Jul 22 13:52:18 2013 +0200
     1.3 @@ -215,17 +215,9 @@
     1.4  fun init_form thy (Prog sc) env =
     1.5    (case get_stac thy sc of
     1.6       NONE => NONE 
     1.7 -             (*error ("init_form: no 1st stac in "^
     1.8 -	      (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) sc))*)
     1.9     | SOME stac => SOME (subst_atomic env stac))
    1.10    | init_form _ _ _ = error "init_form: no match";
    1.11  
    1.12 -(* use"ME/script.sml";
    1.13 -   use"script.sml";
    1.14 -   *)
    1.15 -
    1.16 -
    1.17 -
    1.18  (*the 'iteration-argument' of a stac (args not eval)*)
    1.19  fun itr_arg _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ v) = v
    1.20    | itr_arg _ (Const ("Script.Rewrite",_) $ _ $ _ $ v) = v
    1.21 @@ -236,9 +228,7 @@
    1.22    | itr_arg _ (Const ("Script.Or'_to'_List",_) $ _) = e_term
    1.23    | itr_arg _ (Const ("Script.Tac",_) $ _) = e_term
    1.24    | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term
    1.25 -  | itr_arg thy t = error 
    1.26 -    ("itr_arg not impl. for " ^
    1.27 -    (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt (assoc_thy thy))) t));
    1.28 +  | itr_arg thy t = error ("itr_arg not impl. for " ^ term_to_string'' thy t);
    1.29  (* val t = (term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
    1.30  > itr_arg "Script" t;
    1.31  val it = Free ("e_","RealDef.real") : term 
    1.32 @@ -291,19 +281,15 @@
    1.33  (*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv
    1.34    9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*)
    1.35  fun mk_arg thy d [] = 
    1.36 -    error ("mk_arg: no data for " ^
    1.37 -	   (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) d))
    1.38 +    error ("mk_arg: no data for " ^ term_to_string''' thy d)
    1.39    | mk_arg thy d [t] = 
    1.40      (case dsc_valT d of
    1.41 -	 "una" => [t]
    1.42 -       | "nam" => 
    1.43 -	 [case t of
    1.44 -	      r as (Const ("HOL.eq",_) $ _ $ _) => r
    1.45 -	    | _ => error ("mk_arg: dsc-typ 'nam' applied to non-equality "^
    1.46 -		     (Print_Mode.setmp [] (Syntax.string_of_term
    1.47 -                                               (thy2ctxt thy)) t))]
    1.48 -       | s => error ("mk_arg: not impl. for "^s))
    1.49 -    
    1.50 +	     "una" => [t]
    1.51 +     | "nam" => 
    1.52 +	     [case t of
    1.53 +	        r as (Const ("HOL.eq",_) $ _ $ _) => r
    1.54 +	      | _ => error ("mk_arg: dsc-typ 'nam' applied to non-equality " ^ term_to_string''' thy t)]
    1.55 +        | s => error ("mk_arg: not impl. for "^s))
    1.56    | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts);
    1.57  (* 
    1.58   val d = d_in itm_;
    1.59 @@ -341,7 +327,7 @@
    1.60  > val mI = ("Script","sqrt-equ-test");
    1.61  > val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
    1.62  > val ts = itms2args thy mI itms;
    1.63 -> map (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) ts;
    1.64 +> map (term_to_string''' thy) ts;
    1.65  ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
    1.66  *)
    1.67  
    1.68 @@ -388,9 +374,8 @@
    1.69        (Substitute ((subte2sube o isalist2list) isasub), Empty_Tac_)
    1.70  
    1.71    | stac2tac_ pt thy (Const("Script.Check'_elementwise",_) $ _ $ 
    1.72 -		(set as Const ("Set.Collect",_) $ Abs (_,_,pred))) = 
    1.73 -      (Check_elementwise (Print_Mode.setmp [] (Syntax.string_of_term 
    1.74 -                          (thy2ctxt thy)) pred), (*set*)Empty_Tac_)
    1.75 +      (set as Const ("Set.Collect",_) $ Abs (_,_,pred))) = 
    1.76 +        (Check_elementwise (term_to_string''' thy pred), (*set*)Empty_Tac_)
    1.77  
    1.78    | stac2tac_ pt thy (Const("Script.Or'_to'_List",_) $ _ ) = 
    1.79        (Or_to_List, Empty_Tac_)
    1.80 @@ -436,10 +421,8 @@
    1.81          val f = subpbl (strip_thy dI) pI
    1.82        in (Subproblem (dI, pI),	Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
    1.83        end
    1.84 -
    1.85    | stac2tac_ pt thy t = error 
    1.86 -  ("stac2tac_ TODO: no match for " ^
    1.87 -   (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) t));
    1.88 +      ("stac2tac_ TODO: no match for " ^ term_to_string''' thy t);
    1.89  
    1.90  fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t;
    1.91  
    1.92 @@ -696,8 +679,7 @@
    1.93  
    1.94  fun make_rule thy t =
    1.95    let val ct = cterm_of thy (Trueprop $ t)
    1.96 -  in Thm (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
    1.97 -                           (term_of ct), make_thm ct) end;
    1.98 +  in Thm (term_to_string''' thy (term_of ct), make_thm ct) end;
    1.99  
   1.100  (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;
   1.101     *)