1.1 --- a/src/Tools/isac/Interpret/ctree-basic.sml	Thu Mar 15 12:45:31 2018 +0100
     1.2 +++ b/src/Tools/isac/Interpret/ctree-basic.sml	Thu Mar 15 14:50:29 2018 +0100
     1.3 @@ -240,7 +240,7 @@
     1.4  
     1.5  type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)
     1.6    (int * term list) list * (* assoc-list: args of met*)
     1.7 -  (int * rls) list *       (* assoc-list: tacs already done ///15.9.00*)
     1.8 +  (int * Celem.rls) list * (* assoc-list: tacs already done ///15.9.00*)
     1.9    (int * ets) list *       (* assoc-list: tacs etc. already done*)
    1.10    (string * pos) list;     (* asms * from where*)
    1.11  

     2.1 --- a/src/Tools/isac/calcelems.sml	Thu Mar 15 12:45:31 2018 +0100
     2.2 +++ b/src/Tools/isac/calcelems.sml	Thu Mar 15 14:50:29 2018 +0100
     2.3 @@ -261,7 +261,13 @@
     2.4      val type_to_string'': thyID -> typ -> string
     2.5      val type_to_string''': theory -> typ -> string
     2.6    ----------------------------------------- ^^^ make public -----------------------------------*)
     2.7 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     2.8 +    (* NONE *)
     2.9 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    2.10 +    (* NONE *)
    2.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.12    end
    2.13 +
    2.14  (**)
    2.15  structure Celem(**): CALC_ELEMENT(**) =
    2.16  struct

     3.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml	Thu Mar 15 12:45:31 2018 +0100
     3.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml	Thu Mar 15 14:50:29 2018 +0100
     3.3 @@ -37,9 +37,9 @@
     3.4      val posterms2xml : int -> (Ctree.pos' * term) list -> Celem.xml
     3.5      val precond2xml : int -> bool * Term.term -> Celem.xml
     3.6      val preconds2xml : int -> (bool * Term.term) list -> Celem.xml
     3.7 -    val rls2xml : int -> Celem.thyID * rls -> Celem.xml
     3.8 -    val rule2xml : int -> Celem.guh -> rule -> Celem.xml
     3.9 -    val rules2xml : int -> Celem.guh -> rule list -> Celem.xml
    3.10 +    val rls2xml : int -> Celem.thyID * Celem.rls -> Celem.xml
    3.11 +    val rule2xml : int -> Celem.guh -> Celem.rule -> Celem.xml
    3.12 +    val rules2xml : int -> Celem.guh -> Celem.rule list -> Celem.xml
    3.13      val scr2xml : int -> Celem.scr -> Celem.xml
    3.14      val spec2xml : int -> Celem.spec -> Celem.xml
    3.15      val sub2xml : int -> Term.term * Term.term -> Celem.xml