1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Sun Apr 19 11:07:02 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Sun Apr 19 12:22:37 2020 +0200
     1.3 @@ -339,7 +339,7 @@
     1.4    | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
     1.5                        * tactic Apply_Method metID
     1.6                        * formula term                                        *)
     1.7 -      Celem.metID *  (* key for KEStore                                     *)
     1.8 +      Celem.metID *  (* key for Know_Store                                     *)
     1.9        term option *  (* the first formula of Calc.T. TODO: rm option        *)           
    1.10        Istate_Def.T * (* for the newly started program                       *)
    1.11        Proof.context  (* for the newly started program                       *)
    1.12 @@ -370,7 +370,7 @@
    1.13  
    1.14    | Init_Proof' of TermC.as_string list * Celem.spec
    1.15    | Model_Problem' of (* first step in specifying   *)
    1.16 -    Celem.pblID *     (* key into KEStore           *)
    1.17 +    Celem.pblID *     (* key into Know_Store           *)
    1.18      Model.itm list *  (* the 'untouched' pbl        *)
    1.19      Model.itm list    (* the casually completed met *)
    1.20    | Or_to_List' of term * term