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