1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Tue May 19 12:33:35 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed May 20 12:52:09 2020 +0200
1.3 @@ -384,8 +384,8 @@
1.4 | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
1.5 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
1.6 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
1.7 - | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
1.8 - "," ^ Rule_Set.id rls' ^ "," ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ "," ^ UnparseC.terms asm ^ "))"
1.9 + | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ ", " ^ bool2str pasm ^
1.10 + ", " ^ Rule_Set.id rls' ^ ", " ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ ", " ^ UnparseC.terms asm ^ "))"
1.11 | End_Detail' _ => "End_Detail' xxx"
1.12
1.13 | Derive' rls => "Derive' " ^ Rule_Set.id rls
1.14 @@ -397,7 +397,7 @@
1.15 "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
1.16
1.17 | Empty_Tac_ => "Empty_Tac_"
1.18 - | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
1.19 + | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ ", " ^ id ^ ", " ^ result ^ ")"
1.20
1.21 | Begin_Trans' _ => "Begin_Trans' xxx"
1.22 | End_Trans' _ => "End_Trans' xxx"