1.1 --- a/src/Tools/isac/calcelems.sml	Wed Nov 28 11:46:00 2018 +0100
     1.2 +++ b/src/Tools/isac/calcelems.sml	Wed Nov 28 12:17:42 2018 +0100
     1.3 @@ -61,14 +61,9 @@
     1.4      datatype lrd = D | L | R
     1.5      val trace_rewrite: bool Unsynchronized.ref
     1.6      val depth: int Unsynchronized.ref
     1.7 -    val id_rls: Rule.rls -> string
     1.8 -    val rls2str: Rule.rls -> string
     1.9 -    type errpat
    1.10      val assoc_thy: Rule.theory' -> theory
    1.11 -    eqtype cterm'
    1.12      type loc_
    1.13      val loc_2str: loc_ -> string
    1.14 -    eqtype rew_ord'
    1.15      type thm''
    1.16      val metID2str: string list -> string
    1.17      val e_pblID: pblID
    1.18 @@ -96,7 +91,6 @@
    1.19      val theID2guh: theID -> guh
    1.20      eqtype fillpatID
    1.21      type pbt_ = string * (term * term)
    1.22 -    val e_rew_ord: Rule.subst -> term * term -> bool
    1.23      eqtype xml
    1.24      val cal2guh: string * Rule.thyID -> string -> guh
    1.25      val ketype2str': ketype -> string
    1.26 @@ -106,12 +100,11 @@
    1.27      val theID2thyID: theID -> Rule.thyID
    1.28      val thy2guh: theID -> guh
    1.29      val thypart2guh: theID -> guh
    1.30 -    val ord2guh: string * Rule.thyID -> rew_ord' -> guh
    1.31 +    val ord2guh: string * Rule.theory' -> string -> string
    1.32      val update_hrls: thydata -> Rule.errpatID list -> thydata
    1.33      eqtype iterID
    1.34      eqtype calcID
    1.35      val thm''_of_thm: thm -> thm''
    1.36 -    val rew_ord': (rew_ord' * (Rule.subst -> term * term -> bool)) list Unsynchronized.ref
    1.37      val thm_of_thm: Rule.rule -> thm
    1.38  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.39      val thm2str: thm -> string
    1.40 @@ -128,7 +121,7 @@
    1.41  
    1.42                 
    1.43  (**)
    1.44 -structure Celem(*: CALC_ELEMENT*) =
    1.45 +structure Celem: CALC_ELEMENT =
    1.46  struct
    1.47  (**)
    1.48