1.1 --- a/src/Tools/isac/Interpret/generate.sml	Sun Oct 14 14:43:41 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Sun Oct 14 20:00:27 2012 +0200
     1.3 @@ -3,48 +3,6 @@
     1.4     *)
     1.5  
     1.6  (*.initialize istate for Detail_Set.*)
     1.7 -(*
     1.8 -fun init_istate (Rewrite_Set rls) = 
     1.9 -(* val (Rewrite_Set rls) = (get_obj g_tac pt p);
    1.10 -   *)
    1.11 -    (case assoc_rls rls of
    1.12 -	 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t))
    1.13 -(* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;
    1.14 -   *)
    1.15 -       | Rls {scr=EmptyScr,...} => 
    1.16 -	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.17 -		      ^"use prep_rls for storing rule-sets !")
    1.18 -       | Rls {scr=Script s,...} =>
    1.19 -(* val Rls {scr=Script s,...} = assoc_rls rls;
    1.20 -   *)
    1.21 -	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
    1.22 -       | Seq {scr=EmptyScr,...} => 
    1.23 -	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.24 -		      ^"use prep_rls for storing rule-sets !")
    1.25 -       | Seq {srls=srls,scr=Script s,...} =>
    1.26 -	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
    1.27 -  | init_istate (Rewrite_Set_Inst (subs, rls)) =
    1.28 -(* val (Rewrite_Set_Inst (subs, rls)) = (get_obj g_tac pt p);
    1.29 -   *)
    1.30 -    let val (_, v)::_ = subs2subst (assoc_thy "Isac") subs
    1.31 -    in case assoc_rls rls of
    1.32 -           Rls {scr=EmptyScr,...} => 
    1.33 -	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.34 -			^"use prep_rls for storing rule-sets !")
    1.35 -	 | Rls {scr=Script s,...} =>
    1.36 -	   let val (a1, a2) = two_scr_arg s
    1.37 -	   in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end
    1.38 -	 | Seq {scr=EmptyScr,...} => 
    1.39 -	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.40 -			^"use prep_rls for storing rule-sets !")
    1.41 -(* val Seq {scr=Script s,...} = assoc_rls rls;
    1.42 -   *)
    1.43 -	 | Seq {scr=Script s,...} =>
    1.44 -	   let val (a1, a2) = two_scr_arg s
    1.45 -	   in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end
    1.46 -    end;
    1.47 -*)
    1.48 -(*~~~~~~~~~~~~~~~~~~~~~~copy for dev. until del.~~~~~~~~~~~~~~~~~~~~~~~~~*)
    1.49  fun init_istate (Rewrite_Set rls) t =
    1.50  (* val (Rewrite_Set rls) = (get_obj g_tac pt p);
    1.51     *)
    1.52 @@ -55,14 +13,12 @@
    1.53         | Rls {scr=EmptyScr,...} => 
    1.54  	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.55  		      ^"use prep_rls for storing rule-sets !")
    1.56 -       | Rls {scr=Script s,...} =>
    1.57 -(* val Rls {scr=Script s,...} = assoc_rls rls;
    1.58 -   *)
    1.59 +       | Rls {scr = Prog s,...} =>
    1.60  	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
    1.61         | Seq {scr=EmptyScr,...} => 
    1.62  	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.63  		      ^"use prep_rls for storing rule-sets !")
    1.64 -       | Seq {srls=srls,scr=Script s,...} =>
    1.65 +       | Seq {srls=srls,scr = Prog s,...} =>
    1.66  	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
    1.67  (* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t);
    1.68     *)
    1.69 @@ -73,16 +29,14 @@
    1.70             Rls {scr=EmptyScr,...} => 
    1.71  	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.72  			^"use prep_rls for storing rule-sets !")
    1.73 -	 | Rls {scr=Script s,...} =>
    1.74 +	 | Rls {scr = Prog s,...} =>
    1.75  	   let val (form, bdv) = two_scr_arg s
    1.76  	   in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
    1.77  	   end
    1.78  	 | Seq {scr=EmptyScr,...} => 
    1.79  	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.80  			^"use prep_rls for storing rule-sets !")
    1.81 -(* val Seq {scr=Script s,...} = assoc_rls rls;
    1.82 -   *)
    1.83 -	 | Seq {scr=Script s,...} =>
    1.84 +	 | Seq {scr = Prog s,...} =>
    1.85  	   let val (form, bdv) = two_scr_arg s
    1.86  	   in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
    1.87  	   end