Mercurial Mercurial > wneuper > isa / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/MathEngBasic/tactic.sml
changeset 59902 e7910a62eaf2
parent 59898 68883c046963
child 59903 5037ca1b112b 
     1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Wed Apr 22 11:06:48 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Wed Apr 22 11:23:30 2020 +0200
     1.3 @@ -199,7 +199,7 @@
     1.4  
     1.5  fun input_to_string ma = case ma of
     1.6      Init_Proof (ppc, spec)  => 
     1.7 -      "Init_Proof "^(pair2str (strs2str ppc, Spec.spec2str spec))
     1.8 +      "Init_Proof "^(pair2str (strs2str ppc, Spec.to_string spec))
     1.9    | Model_Problem           => "Model_Problem "
    1.10    | Refine_Tacitly pblID    => "Refine_Tacitly " ^ strs2str pblID 
    1.11    | Refine_Problem pblID    => "Refine_Problem " ^ strs2str pblID 
    1.12 @@ -409,7 +409,7 @@
    1.13    | Take' of term
    1.14  
    1.15  fun string_of ma = case ma of
    1.16 -    Init_Proof' (ppc, spec)  => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.spec2str spec)
    1.17 +    Init_Proof' (ppc, spec)  => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.to_string spec)
    1.18    | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
    1.19    | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
    1.20      strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
wneuper/isa