1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Wed Dec 21 11:27:22 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Thu Dec 22 10:25:49 2016 +0100
     1.3 @@ -7,31 +7,31 @@
     1.4  sig
     1.5    type calcstate
     1.6    type calcstate'
     1.7 -  datatype appl = Appl of tac_ | Notappl of string
     1.8 -  val nxt_specify_init_calc : fmz -> calcstate
     1.9 -  val specify : tac_ -> pos' -> cid -> ptree ->
    1.10 -    (posel list * pos_) * ((posel list * pos_) * istate) * Generate.mout * tac * safe * ptree
    1.11 -  val nxt_specif : tac -> ptree * (pos * pos_) -> calcstate'
    1.12 -  val nxt_spec : pos_ -> bool -> ori list -> spec -> itm list * itm list ->
    1.13 -    (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> pos_ * tac
    1.14 +  datatype appl = Appl of Ctree.tac_ | Notappl of string
    1.15 +  val nxt_specify_init_calc : Ctree.fmz -> calcstate
    1.16 +  val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ptree ->
    1.17 +    Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ptree
    1.18 +  val nxt_specif : Ctree.tac -> Ctree.ptree * Ctree.pos' -> calcstate'
    1.19 +  val nxt_spec : Ctree.pos_ -> bool -> ori list -> spec -> itm list * itm list ->
    1.20 +    (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac
    1.21  
    1.22 -  val reset_calchead : ptree * pos' -> ptree * pos'
    1.23 -  val get_ocalhd : ptree * pos' -> ocalhd
    1.24 +  val reset_calchead : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
    1.25 +  val get_ocalhd : Ctree.ptree * Ctree.pos' -> Ctree.ocalhd
    1.26    val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool
    1.27 -  val all_modspec : ptree * pos' -> ptree * pos' 
    1.28 +  val all_modspec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' 
    1.29  
    1.30    val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list
    1.31    val insert_ppc' : itm -> itm list -> itm list
    1.32  
    1.33 -  val complete_mod : ptree * pos' -> ptree * pos'
    1.34 -  val is_complete_mod : ptree * pos' -> bool
    1.35 -  val complete_spec : ptree * pos' -> ptree * pos' 
    1.36 -  val is_complete_spec : ptree * pos' -> bool
    1.37 +  val complete_mod : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
    1.38 +  val is_complete_mod : Ctree.ptree * Ctree.pos' -> bool
    1.39 +  val complete_spec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
    1.40 +  val is_complete_spec : Ctree.ptree * Ctree.pos' -> bool
    1.41    val some_spec : spec -> spec -> spec
    1.42    (* these could go to Ctree ..*)
    1.43 -  val show_pt : ptree -> unit
    1.44 -  val pt_extract : ptree * (posel list * pos_) -> ptform * tac option * term list 
    1.45 -  val get_interval : int list * pos_ -> pos' -> int -> ptree -> (pos' * term) list
    1.46 +  val show_pt : Ctree.ptree -> unit
    1.47 +  val pt_extract : Ctree.ptree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list 
    1.48 +  val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ptree -> (Ctree.pos' * term) list
    1.49  
    1.50    val match_ags : theory -> pat list -> term list -> ori list
    1.51    val match_ags_msg : pblID -> term -> term list -> unit
    1.52 @@ -56,7 +56,7 @@
    1.53  
    1.54  structure Chead(**): CALC_HEAD(**) =
    1.55  struct
    1.56 -
    1.57 +open Ctree
    1.58  (* datatypes *)
    1.59  
    1.60  (* the state wich is stored after each step of calculation; it contains