1.1 --- a/src/Tools/isac/ME/inform.sml	Thu Aug 19 15:02:06 2010 +0200
     1.2 +++ b/src/Tools/isac/ME/inform.sml	Thu Aug 19 15:20:53 2010 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4      val imodel2fstr : iitem list -> (string * cterm') list
     1.5  
     1.6      
     1.7 -    val Isac : 'a -> Theory.theory
     1.8 +    val Isac : 'a -> theory
     1.9      val appl_add' :
    1.10         theory' ->
    1.11         SpecifyTools.ori list ->
    1.12 @@ -67,7 +67,7 @@
    1.13     (* val filter_sep : ('a -> bool) -> 'a list -> 'a list * 'a list *)
    1.14     (* val flattup2 : 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e *)
    1.15     (* val fstr2itm_ :
    1.16 -       Theory.theory ->
    1.17 +       theory ->
    1.18         (''a * (Term.term * Term.term)) list ->
    1.19         ''a * string -> int list * bool * ''a * SpecifyTools.itm_ *)
    1.20      val inform :
    1.21 @@ -85,7 +85,7 @@
    1.22      val oris2itms :
    1.23         'a -> int -> SpecifyTools.ori list -> SpecifyTools.itm list
    1.24     (* val par2fstr : SpecifyTools.itm -> string * cterm' *)
    1.25 -   (* val parsitm : Theory.theory -> SpecifyTools.itm -> SpecifyTools.itm *)
    1.26 +   (* val parsitm : theory -> SpecifyTools.itm -> SpecifyTools.itm *)
    1.27      val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
    1.28     (* val unknown_expl :
    1.29         theory' ->