1.1 --- a/src/Tools/isac/Interpret/inform.sml	Wed Nov 13 12:45:24 2013 +0000
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Wed Nov 13 12:53:39 2013 +0000
     1.3 @@ -8,9 +8,8 @@
     1.4  *)
     1.5  
     1.6  signature INFORM =
     1.7 -  sig 
     1.8 +  sig
     1.9  
    1.10 -    type castab
    1.11      type icalhd
    1.12  
    1.13     (* type iitem *)
    1.14 @@ -42,7 +41,6 @@
    1.15         (Term.term * Term.term list) list ->
    1.16         pblID * SpecifyTools.itm list * metID * SpecifyTools.itm list *
    1.17         (bool * Term.term) list  *)
    1.18 -    val castab : castab Unsynchronized.ref
    1.19      val compare_step :
    1.20         calcstate' -> Term.term -> string * calcstate'
    1.21     (* val concat_deriv :
    1.22 @@ -135,24 +133,6 @@
    1.23  
    1.24  fun flattup2 (a,(b,c,d,e)) = (a,b,c,d,e);
    1.25  
    1.26 -
    1.27 -
    1.28 -(*.association list with cas-commands, for generating a complete calc-head.*)
    1.29 -type castab = 
    1.30 -     (term *         (*cas-command, eg. 'solve'*)
    1.31 -      (spec * 	     (*theory, problem, method*)
    1.32 -
    1.33 -       		     (*the function generating a kind of formalization*)
    1.34 -       (term list -> (*the arguments of the cas-command, eg. (x+1=2, x)*)
    1.35 -	(term *      (*description of an element*)
    1.36 -	 term list)  (*value of the element (always put into a list)*)
    1.37 -	    list)))  (*of elements in the formalization*)
    1.38 -	 list;       (*of cas-entries in the association list*)
    1.39 -
    1.40 -val castab = Unsynchronized.ref ([]: castab);
    1.41 -
    1.42 -fun assoc_castab x = assoc (!castab, x);
    1.43 -
    1.44  fun cas_input_ ((dI,pI,mI): spec) dtss = (*WN110515 reconsider thy..ctxt*)
    1.45    let
    1.46      val thy = assoc_thy dI