1.1 --- a/TODO.md	Wed Jul 27 14:04:04 2022 +0200
     1.2 +++ b/TODO.md	Wed Jul 27 14:14:16 2022 +0200
     1.3 @@ -97,8 +97,6 @@
     1.4      - this proposal presumable involves hacking of parsers -- is there a better way?
     1.5      - implementation and tests have solution for (a) above as a prerequisite.
     1.6  
     1.7 -* WN: rename in Formalise: type spec = Model_Def.form_spec;
     1.8 -                           type refs = Model_Def.form_refs;
     1.9  * WN: as soon as parsing in Outer_Syntax.command..‹Example› works, implement in Calculation
    1.10    - init_ctree, update_status, check_input
    1.11  

     2.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml	Wed Jul 27 14:04:04 2022 +0200
     2.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml	Wed Jul 27 14:14:16 2022 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  
     2.5    type form_T
     2.6    type form_model
     2.7 -  type form_spec
     2.8 +  type form_refs
     2.9    val form_empty : form_T
    2.10  
    2.11    type variant
    2.12 @@ -48,8 +48,8 @@
    2.13  (** definitions for Formalise.T **)
    2.14  
    2.15  type form_model = TermC.as_string list;
    2.16 -type form_spec = References_Def.T;
    2.17 -type form_T = form_model * form_spec;
    2.18 +type form_refs = References_Def.T;
    2.19 +type form_T = form_model * form_refs;
    2.20  val form_empty = ([], References_Def.empty);
    2.21  
    2.22  type variant = int;

     3.1 --- a/src/Tools/isac/Specify/formalise.sml	Wed Jul 27 14:04:04 2022 +0200
     3.2 +++ b/src/Tools/isac/Specify/formalise.sml	Wed Jul 27 14:14:16 2022 +0200
     3.3 @@ -29,11 +29,11 @@
     3.4  (**)
     3.5  
     3.6  type model = Model_Def.form_model;
     3.7 -type spec = Model_Def.form_spec;
     3.8 +type spec = Model_Def.form_refs;
     3.9  
    3.10  (* a formalization of an example contains data 
    3.11     sufficient for mechanically finding the solution for the example.
    3.12 -   FIXME.WN051014: dont store form_T = (_,form_spec) in the PblObj, this is done in origin *)
    3.13 +   FIXME.WN051014: dont store form_T = (_,form_refs) in the PblObj, this is done in origin *)
    3.14  type T = Model_Def.form_T;
    3.15  val empty = Model_Def.form_empty;
    3.16