1.1 --- a/src/Tools/isac/Interpret/script.sml	Fri May 20 14:08:14 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri May 20 14:49:07 2011 +0200
     1.3 @@ -652,28 +652,22 @@
     1.4    | tac_2tac (Specify_Problem' (dI,_))      = Specify_Problem dI
     1.5    | tac_2tac (Specify_Method' (dI,_,_))     = Specify_Method dI
     1.6    
     1.7 -  | tac_2tac (Rewrite' (thy,rod,erls,put,(thmID,thm),f,(f',asm))) =
     1.8 -    Rewrite (thmID,thm)
     1.9 +  | tac_2tac (Rewrite' (thy,rod,erls,put,(thmID,thm),f,(f',asm))) = Rewrite (thmID,thm)
    1.10  
    1.11    | tac_2tac (Rewrite_Inst' (thy,rod,erls,put,sub,(thmID,thm),f,(f',asm)))=
    1.12 -    Rewrite_Inst (subst2subs sub,(thmID,thm))
    1.13 +      Rewrite_Inst (subst2subs sub,(thmID,thm))
    1.14  
    1.15 -  | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) = 
    1.16 -    Rewrite_Set (id_rls rls)
    1.17 -
    1.18 -  | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) = 
    1.19 -    Detail_Set (id_rls rls)
    1.20 +  | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) = Rewrite_Set (id_rls rls)
    1.21 +  | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) = Detail_Set (id_rls rls)
    1.22  
    1.23    | tac_2tac (Rewrite_Set_Inst' (thy,put,sub,rls,f,(f',asm))) = 
    1.24 -    Rewrite_Set_Inst (subst2subs sub,id_rls rls)
    1.25 -
    1.26 +      Rewrite_Set_Inst (subst2subs sub,id_rls rls)
    1.27    | tac_2tac (Detail_Set_Inst' (thy,put,sub,rls,f,(f',asm))) = 
    1.28 -    Detail_Set_Inst (subst2subs sub,id_rls rls)
    1.29 +      Detail_Set_Inst (subst2subs sub,id_rls rls)
    1.30  
    1.31    | tac_2tac (Calculate' (thy,op_,t,(t',thm'))) = Calculate (op_)
    1.32  
    1.33 -  | tac_2tac (Check_elementwise' (consts,pred,consts')) =
    1.34 -    Check_elementwise pred
    1.35 +  | tac_2tac (Check_elementwise' (consts,pred,consts')) = Check_elementwise pred
    1.36  
    1.37    | tac_2tac (Or_to_List' _) = Or_to_List
    1.38    | tac_2tac (Take' term) = Take (term2str term)
    1.39 @@ -681,14 +675,11 @@
    1.40  
    1.41    | tac_2tac (Tac_ (_,f,id,f')) = Tac id
    1.42  
    1.43 -  | tac_2tac (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = 
    1.44 -		  Subproblem (domID, pblID)
    1.45 -  | tac_2tac (Check_Postcond' (pblID, _)) = 
    1.46 -		  Check_Postcond pblID
    1.47 +  | tac_2tac (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
    1.48 +  | tac_2tac (Check_Postcond' (pblID, _)) = Check_Postcond pblID
    1.49    | tac_2tac Empty_Tac_ = Empty_Tac
    1.50 -
    1.51    | tac_2tac m = 
    1.52 -  error ("tac_2tac: not impl. for "^(tac_2str m));
    1.53 +      error ("tac_2tac: not impl. for "^(tac_2str m));
    1.54  
    1.55  
    1.56