1.1 --- a/src/Tools/isac/calcelems.sml	Thu Mar 15 10:17:44 2018 +0100
     1.2 +++ b/src/Tools/isac/calcelems.sml	Thu Mar 15 12:42:04 2018 +0100
     1.3 @@ -190,6 +190,10 @@
     1.4      eqtype calcID
     1.5      val thm''_of_thm: thm -> thm''
     1.6      val rew_ord': (rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
     1.7 +    val merge_rls: string -> rls -> rls -> rls
     1.8 +    val e_rrlsstate: rrlsstate
     1.9 +    val thm_of_thm: rule -> thm
    1.10 +    val remove_rls: string -> rls -> rule list -> rls
    1.11  
    1.12  (*---------------------- ^^^ make public on a minimalist way down to Build?Isac -----------------
    1.13      val Html_default: theID -> thydata
    1.14 @@ -205,7 +209,6 @@
    1.15      val e_rew_ord': rew_ord'
    1.16      val e_rew_ord_: subst -> term * term -> bool
    1.17      val e_rfuns: scr
    1.18 -    val e_rrlsstate: rrlsstate
    1.19      val e_scr: scr
    1.20      val e_subst: (term * term) list
    1.21      val e_theID: string list
    1.22 @@ -225,14 +228,12 @@
    1.23      val memrls: rule -> rls -> bool
    1.24      val merge_ids: rls -> rls -> string
    1.25      val merge_ptyps': 'a ptyp list -> 'a ptyp list -> 'a ptyp list
    1.26 -    val merge_rls: string -> rls -> rls -> rls
    1.27      val overwritelthy: theory -> (rls' * (string * rls)) list * (rls' * rls) list -> (rls' * (string * rls)) list
    1.28      val partID: theory -> string
    1.29      val pat2str: pat -> string
    1.30      val pblID2str: string list -> string
    1.31      val pbt2str: pbt -> string
    1.32      val progthys: unit -> theory list
    1.33 -    val remove_rls: string -> rls -> rule list -> rls
    1.34      val rep_rrls:
    1.35         rls -> {attach_form: rule list list -> term -> term -> (rule * (term * term list)) list,
    1.36                 calc: calc list,
    1.37 @@ -255,7 +256,6 @@
    1.38      val theory2str': theory -> string
    1.39      val thm2str: thm -> string
    1.40      eqtype thmDeriv
    1.41 -    val thm_of_thm: rule -> thm
    1.42      val thy2ctxt: theory -> Proof.context
    1.43      val type_to_string': Proof.context -> typ -> string
    1.44      val type_to_string'': thyID -> typ -> string