1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Fri Apr 10 16:16:09 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Fri Apr 10 18:32:36 2020 +0200
     1.3 @@ -218,8 +218,8 @@
     1.4    | Free_Solve              => "Free_Solve"
     1.5  
     1.6    | Rewrite_Inst (subs, (id, thm)) =>
     1.7 -    "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> UnparseC.term2str)))
     1.8 -  | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> UnparseC.term2str)
     1.9 +    "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> UnparseC.term)))
    1.10 +  | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> UnparseC.term)
    1.11    | Rewrite_Set_Inst (subs, rls) => 
    1.12      "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
    1.13    | Rewrite_Set rls         => "Rewrite_Set " ^ quote rls
    1.14 @@ -429,7 +429,7 @@
    1.15  
    1.16    | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
    1.17    | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
    1.18 -      (spair2str (strs2str pblID, UnparseC.term2str scval))
    1.19 +      (spair2str (strs2str pblID, UnparseC.term scval))
    1.20  
    1.21    | Free_Solve' => "Free_Solve'"
    1.22  
    1.23 @@ -437,7 +437,7 @@
    1.24    | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
    1.25    | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
    1.26    | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
    1.27 -    "," ^ Rule_Set.id rls' ^ "," ^ UnparseC.term2str f ^ ",(" ^ UnparseC.term2str f' ^ "," ^ UnparseC.terms2str asm ^ "))"
    1.28 +    "," ^ Rule_Set.id rls' ^ "," ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ "," ^ UnparseC.terms asm ^ "))"
    1.29    | End_Detail' _ => "End_Detail' xxx"
    1.30    | Detail_Set' _ => "Detail_Set' xxx"
    1.31    | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
    1.32 @@ -480,7 +480,7 @@
    1.33    | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
    1.34  
    1.35    | input_from_T (Or_to_List' _) = Or_to_List
    1.36 -  | input_from_T (Take' term) = Take (UnparseC.term2str term)
    1.37 +  | input_from_T (Take' term) = Take (UnparseC.term term)
    1.38    | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Selem.subte2sube subte) 
    1.39    | input_from_T (Tac_ (_, _, id, _)) = Tac id
    1.40