1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Mon Apr 27 12:36:21 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Mon Apr 27 16:37:56 2020 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4        (*Istate.T *       ?       *)
     1.5        Proof.context * (* derived from prog. in ???  *)
     1.6        term            (* ?UNUSED, e.g."Subproblem\n (''Test'',\n  ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n   ''test'')" *)
     1.7 -  | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_equality * term * term
     1.8 +  | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
     1.9    | Tac_ of theory * string * string * string
    1.10    | Take' of term
    1.11    val string_of: T -> string
    1.12 @@ -101,7 +101,7 @@
    1.13    | Specify_Theory of ThyC.id
    1.14    | Subproblem of ThyC.id * Problem.id
    1.15  
    1.16 -  | Substitute of Subst.tyty
    1.17 +  | Substitute of Subst.input
    1.18    | Tac of string
    1.19    | Take of TermC.as_string | Take_Inst of TermC.as_string
    1.20    val input_to_string : input -> string
    1.21 @@ -193,7 +193,7 @@
    1.22    | Specify_Theory of ThyC.id
    1.23    | Subproblem of ThyC.id * Problem.id (* WN0509 drop *)
    1.24  
    1.25 -  | Substitute of Subst.tyty
    1.26 +  | Substitute of Subst.input
    1.27    | Tac of string               (* WN0509 drop *)
    1.28    | Take of TermC.as_string | Take_Inst of TermC.as_string
    1.29  
    1.30 @@ -228,7 +228,7 @@
    1.31    | End_Detail              => "End_Detail"
    1.32    | Derive rls'             => "Derive " ^ rls' 
    1.33    | Calculate op_           => "Calculate " ^ op_
    1.34 -  | Substitute sube         => "Substitute " ^ Subst.tyty_to_string sube	     
    1.35 +  | Substitute sube         => "Substitute " ^ Subst.string_eqs_to_string sube	     
    1.36    | Apply_Assumption ct's   => "Apply_Assumption " ^ strs2str ct's
    1.37  
    1.38    | Take cterm'             => "Take " ^ quote cterm'
    1.39 @@ -402,7 +402,7 @@
    1.40    | Substitute' of           
    1.41      Rule_Def.rew_ord_ *          (* for re-calculation                        *)
    1.42      Rule_Set.T *               (* for re-calculation                        *)
    1.43 -    Subst.as_equality *            (* the 'substitution': terms of type bool    *)
    1.44 +    Subst.as_eqs *            (* the 'substitution': terms of type bool    *)
    1.45      term *                   (* to be substituted into                    *)
    1.46      term                     (* resulting from the substitution           *)
    1.47    | Tac_ of theory * string * string * string
    1.48 @@ -481,7 +481,7 @@
    1.49  
    1.50    | input_from_T (Or_to_List' _) = Or_to_List
    1.51    | input_from_T (Take' term) = Take (UnparseC.term term)
    1.52 -  | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Subst.eqs_to_tyty subte) 
    1.53 +  | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Subst.eqs_to_input subte) 
    1.54    | input_from_T (Tac_ (_, _, id, _)) = Tac id
    1.55  
    1.56    | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)