1.1 --- a/src/Tools/isac/Interpret/ctree.sml	Wed Nov 13 12:45:24 2013 +0000
     1.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Wed Nov 13 12:53:39 2013 +0000
     1.3 @@ -288,13 +288,6 @@
     1.4  
     1.5  datatype con = land | lor;
     1.6  
     1.7 -
     1.8 -type spec = 
     1.9 -     domID * (*WN.12.03: is replaced by thy from get_met ?FIXME? in:
    1.10 -	      specify (Init_Proof..), nxt_specify_init_calc,
    1.11 -	      assod (.SubProblem...), stac2tac (.SubProblem...)*)
    1.12 -     pblID * 
    1.13 -     metID;
    1.14  fun spec2str ((dom,pbl,met)(*:spec*)) = 
    1.15    "(" ^ (quote dom) ^ ", " ^ (strs2str pbl) ^ 
    1.16    ", " ^ (strs2str met) ^ ")";

     2.1 --- a/src/Tools/isac/Interpret/inform.sml	Wed Nov 13 12:45:24 2013 +0000
     2.2 +++ b/src/Tools/isac/Interpret/inform.sml	Wed Nov 13 12:53:39 2013 +0000
     2.3 @@ -8,9 +8,8 @@
     2.4  *)
     2.5  
     2.6  signature INFORM =
     2.7 -  sig 
     2.8 +  sig
     2.9  
    2.10 -    type castab
    2.11      type icalhd
    2.12  
    2.13     (* type iitem *)
    2.14 @@ -42,7 +41,6 @@
    2.15         (Term.term * Term.term list) list ->
    2.16         pblID * SpecifyTools.itm list * metID * SpecifyTools.itm list *
    2.17         (bool * Term.term) list  *)
    2.18 -    val castab : castab Unsynchronized.ref
    2.19      val compare_step :
    2.20         calcstate' -> Term.term -> string * calcstate'
    2.21     (* val concat_deriv :
    2.22 @@ -135,24 +133,6 @@
    2.23  
    2.24  fun flattup2 (a,(b,c,d,e)) = (a,b,c,d,e);
    2.25  
    2.26 -
    2.27 -
    2.28 -(*.association list with cas-commands, for generating a complete calc-head.*)
    2.29 -type castab = 
    2.30 -     (term *         (*cas-command, eg. 'solve'*)
    2.31 -      (spec * 	     (*theory, problem, method*)
    2.32 -
    2.33 -       		     (*the function generating a kind of formalization*)
    2.34 -       (term list -> (*the arguments of the cas-command, eg. (x+1=2, x)*)
    2.35 -	(term *      (*description of an element*)
    2.36 -	 term list)  (*value of the element (always put into a list)*)
    2.37 -	    list)))  (*of elements in the formalization*)
    2.38 -	 list;       (*of cas-entries in the association list*)
    2.39 -
    2.40 -val castab = Unsynchronized.ref ([]: castab);
    2.41 -
    2.42 -fun assoc_castab x = assoc (!castab, x);
    2.43 -
    2.44  fun cas_input_ ((dI,pI,mI): spec) dtss = (*WN110515 reconsider thy..ctxt*)
    2.45    let
    2.46      val thy = assoc_thy dI

     3.1 --- a/src/Tools/isac/calcelems.sml	Wed Nov 13 12:45:24 2013 +0000
     3.2 +++ b/src/Tools/isac/calcelems.sml	Wed Nov 13 12:53:39 2013 +0000
     3.3 @@ -381,6 +381,27 @@
     3.4  val e_metID = ["e_metID"]:metID;
     3.5  val metID2str = strs2str;
     3.6  
     3.7 +type spec = 
     3.8 +     domID * (*WN.12.03: is replaced by thy from get_met ?FIXME? in:
     3.9 +	      specify (Init_Proof..), nxt_specify_init_calc,
    3.10 +	      assod (.SubProblem...), stac2tac (.SubProblem...)*)
    3.11 +     pblID * 
    3.12 +     metID;
    3.13 +
    3.14 +(*.association list with cas-commands, for generating a complete calc-head.*)
    3.15 +type castab = 
    3.16 +     (term *         (*cas-command, eg. 'solve'*)
    3.17 +      (spec * 	     (*theory, problem, method*)
    3.18 +
    3.19 +       		     (*the function generating a kind of formalization*)
    3.20 +       (term list -> (*the arguments of the cas-command, eg. (x+1=2, x)*)
    3.21 +	(term *      (*description of an element*)
    3.22 +	 term list)  (*value of the element (always put into a list)*)
    3.23 +	    list)))  (*of elements in the formalization*)
    3.24 +	 list;       (*of cas-entries in the association list*)
    3.25 +
    3.26 +val castab = Unsynchronized.ref ([]: castab);
    3.27 +
    3.28  (*either theID or pblID or metID*)
    3.29  type kestoreID = string list;
    3.30  val e_kestoreID = ["e_kestoreID"];