1.1 --- a/src/Tools/isac/BaseDefinitions/celem-5.sml	Sun Apr 19 16:43:53 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/celem-5.sml	Mon Apr 20 15:54:19 2020 +0200
     1.3 @@ -1,18 +1,17 @@
     1.4 -(* Title:  BaseDefinitions/celem-5.sml
     1.5 +(* Title:  BaseDefinitions/problem-def.sml
     1.6     Author: Walther Neuper
     1.7     (c) due to copyright terms
     1.8  
     1.9 -          *)
    1.10 +Will be enhanced by Problem later.
    1.11 +*)
    1.12  signature CALCELEMENT_5 =
    1.13 -(*/------- to Celem5 -------\*)
    1.14 -(*\------- to Celem5 -------/*)
    1.15  sig
    1.16 -(*/------- to Celem5 -------\*)
    1.17    type pbt
    1.18    type ptyps
    1.19    val pbts2str: pbt list -> string
    1.20    val e_Ptyp: pbt Store.ptyp
    1.21 -(*\------- to Celem5 -------/*)
    1.22 +(*vvv check_unique*)
    1.23 +  val check_pblguh_unique: Check_Unique.guh -> pbt Store.ptyp list -> unit
    1.24  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.25    val e_pbt: pbt
    1.26  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.27 @@ -27,7 +26,7 @@
    1.28  
    1.29  (*/------- to Celem5 -------\*)
    1.30  type pbt = 
    1.31 -  {guh : Spec.guh,         (* unique within this isac-knowledge                               *)
    1.32 +  {guh : Check_Unique.guh,         (* unique within this isac-knowledge                               *)
    1.33    mathauthors : string list, (* copyright                                                *)
    1.34    init : Spec.pblID,       (* to start refinement with                                        *)
    1.35    thy  : theory,      (* which allows to compile that pbt
    1.36 @@ -60,4 +59,7 @@
    1.37  type ptyps = (pbt Store.ptyp) list
    1.38  (*\------- to Celem5 -------/*)
    1.39  
    1.40 +val check_pblguh_unique =
    1.41 +  Check_Unique.messsage (Check_Unique.collect (#guh : pbt -> Check_Unique.guh));
    1.42 +
    1.43  (**)end(**)