src/Tools/isac/Interpret/inform.sml
changeset 59271 7a02202e4577
parent 59269 1da53d1540fe
child 59272 1d3ef477d9c8
     1.1 --- a/src/Tools/isac/Interpret/inform.sml	Mon Dec 19 09:02:41 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Mon Dec 19 10:37:44 2016 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4    val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
     1.5    val cas_input : term -> (ptree * ocalhd) option
     1.6    val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
     1.7 -  val compare_step : Ctree.taci list * pos' list * (ptree * pos') -> term -> string * Chead.calcstate'
     1.8 +  val compare_step : Generate.taci list * pos' list * (ptree * pos') -> term -> string * Chead.calcstate'
     1.9    val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
    1.10    val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
    1.11      rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list
    1.12 @@ -389,7 +389,7 @@
    1.13      then
    1.14         let
    1.15           val tacis' = map (mk_tacis rew_ord erls) der;
    1.16 -		     val (c', ptp) = Ctree.embed_deriv tacis' ptp;
    1.17 +		     val (c', ptp) = Generate.embed_deriv tacis' ptp;
    1.18  	     in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
    1.19       else 
    1.20  	     if pos = ([], Res) (*TODO: we should stop earlier with trying subproblems *)