1.1 --- a/src/Tools/isac/calcelems.sml	Thu Mar 15 15:48:52 2018 +0100
     1.2 +++ b/src/Tools/isac/calcelems.sml	Fri Mar 23 10:14:39 2018 +0100
     1.3 @@ -195,7 +195,7 @@
     1.4      val thm_of_thm: rule -> thm
     1.5      val remove_rls: string -> rls -> rule list -> rls
     1.6  
     1.7 -(*---------------------- ^^^ make public on a minimalist way down to Build?Isac -----------------
     1.8 +(*---------------------- vvv^ make public for Test_Isac ------------------------------------
     1.9      val Html_default: theID -> thydata
    1.10      val a_term: term
    1.11      val a_type: typ
    1.12 @@ -204,7 +204,6 @@
    1.13      val e_guh: guh
    1.14      val e_kestoreID: string list
    1.15      val e_met: met
    1.16 -    val e_pbt: pbt
    1.17      val e_pbt_: pbt_
    1.18      val e_rew_ord': rew_ord'
    1.19      val e_rew_ord_: subst -> term * term -> bool
    1.20 @@ -222,7 +221,6 @@
    1.21      val insert_merge_rls: rlss_elem -> rlss_elem list -> rlss_elem list
    1.22      val insthy: 'a -> 'b * 'c -> 'b * ('a * 'c)
    1.23      val kestoreID2str: string list -> string
    1.24 -    val knowthys: unit -> theory list
    1.25      val ldr2str: lrd -> string
    1.26      val lim_rewrite: int Unsynchronized.ref
    1.27      val memrls: rule -> rls -> bool
    1.28 @@ -245,25 +243,27 @@
    1.29                 next_rule: rule list list -> term -> rule option, normal_form: term -> (term * term list) option, prepat: (term list * term) list, rew_ord: rew_ord}
    1.30      val rep_thm_G': rule -> string * thm
    1.31      val str2ketype: string -> ketype
    1.32 -    val string_of_thm: thm -> string
    1.33 -    val string_of_thm': theory -> thm -> string
    1.34      val string_to_bool: string -> bool
    1.35      type subs' = (cterm' * cterm') list
    1.36 -    val term_to_string'': thyID -> term -> string
    1.37 -    val terms2str': term list -> string
    1.38      type thehier = thydata ptyp list
    1.39      val theory2str': theory -> string
    1.40 -    val thm2str: thm -> string
    1.41      eqtype thmDeriv
    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
    1.45      val type_to_string''': theory -> typ -> string
    1.46 -  ----------------------------------------- ^^^ make public -----------------------------------*)
    1.47 +  ---------------------- vvv^ make public for Test_Isac ------------------------------------*)
    1.48  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.49      (* NONE *)
    1.50  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.51      val terms2strs: term list -> string list
    1.52 +    val terms2str': term list -> string
    1.53 +    val term_to_string'': thyID -> term -> string
    1.54 +    val string_of_thm': theory -> thm -> string
    1.55 +    val string_of_thm: thm -> string
    1.56 +    val knowthys: unit -> theory list
    1.57 +    val thm2str: thm -> string
    1.58 +    val e_pbt: pbt
    1.59  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.60    end
    1.61  
    1.62 @@ -783,11 +783,12 @@
    1.63    The association list is required for 'rewrite.."rew_ord"..'
    1.64    WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
    1.65  val rew_ord' = Unsynchronized.ref
    1.66 -        ([]:(rew_ord' *        (*the key for the association list         *)
    1.67 -	     (subst 	       (*the bound variables - they get high order*)
    1.68 -	      -> (term * term) (*(t1, t2) to be compared                  *)
    1.69 -	      -> bool))        (*if t1 <= t2 then true else false         *)
    1.70 -		list);         (*association list                         *)
    1.71 +  ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
    1.72 +	: (rew_ord' *         (* the key for the association list         *)
    1.73 +	    (subst 	          (* the bound variables - they get high order*)
    1.74 +	     -> (term * term) (* (t1, t2) to be compared                  *)
    1.75 +	     -> bool))        (* if t1 <= t2 then true else false         *)
    1.76 +		list);              (* association list                         *)
    1.77  
    1.78  (* NOT ACCEPTED BY struct
    1.79  rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),