1.1 --- a/src/Tools/isac/calcelems.sml	Fri May 10 15:59:58 2019 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Mon May 27 19:28:40 2019 +0200
     1.3 @@ -1,4 +1,5 @@
     1.4 -(* elements of calculations.
     1.5 +(* ~~/src/Tools/isac/calcelems.sml
     1.6 +   elements of calculations.
     1.7     they are partially held in association lists as ref's for
     1.8     switching language levels (meta-string, object-values).                                  
     1.9     in order to keep these ref's during re-evaluation of code,                       
    1.10 @@ -108,6 +109,7 @@
    1.11      val thm_of_thm: Rule.rule -> thm
    1.12  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.13      val thm2str: thm -> string
    1.14 +    val pats2str' : pat list -> string
    1.15      val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list ->
    1.16        thydata ptyp list
    1.17  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.18 @@ -121,10 +123,8 @@
    1.19    (Rule.rls' * (string * Rule.rls)) list  end
    1.20  
    1.21                 
    1.22 -(**)
    1.23 -structure Celem: CALC_ELEMENT =
    1.24 +structure Celem(**): CALC_ELEMENT(**) =
    1.25  struct
    1.26 -(**)
    1.27  
    1.28  val linefeed = (curry op^) "\n"; (* ?\<longrightarrow> libraryC ?*)
    1.29  type authors = string list;
    1.30 @@ -496,6 +496,9 @@
    1.31  fun pat2str ((field, (dsc, id)) : pat) = 
    1.32    pair2str (field, pair2str (Rule.term2str dsc, Rule.term2str id))
    1.33  fun pats2str pats = (strs2str o (map pat2str)) pats
    1.34 +fun pat2str' ((field, (dsc, id)) : pat) = 
    1.35 +  pair2str (field, pair2str (Rule.term2str dsc, Rule.term2str id)) ^ "\n"
    1.36 +fun pats2str' pats = (strs2str o (map pat2str')) pats
    1.37  
    1.38  (* types for problems models (TODO rename to specification models) *)
    1.39  type pbt_ =