src/Tools/isac/MathEngBasic/tactic.sml
changeset 59997 46fe5a8c3911
parent 59985 9aaeab7d38b6
child 60017 cdcc5eba067b
     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"