1.1 --- a/src/Tools/isac/Interpret/inform.sml	Sat Jan 21 12:01:30 2017 +0100
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Sat Jan 21 12:32:32 2017 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4    val fetchErrorpatterns : Ctree.tac -> errpatID list
     1.5    val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
     1.6    val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
     1.7 -  val find_fillpatterns : Ctree.state -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list
     1.8 +  val find_fillpatterns : Ctree.state -> errpatID -> (fillpatID * term * thm * Selem.subs option) list
     1.9    val is_exactly_equal : Ctree.state -> string -> string * Ctree.tac
    1.10  
    1.11  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.12 @@ -91,7 +91,7 @@
    1.13  	  val its = Specify.add_id its_
    1.14  	  val mits = map flattup2 its
    1.15  	  val pre = check_preconds thy prls pre mits
    1.16 -    val ctxt = Ctree.e_ctxt (*WN110515 cas_input_ DOESNT WORK*)
    1.17 +    val ctxt = Selem.e_ctxt (*WN110515 cas_input_ DOESNT WORK*)
    1.18    in (pI, pits: itm list, mI, mits: itm list, pre, ctxt) end;
    1.19  
    1.20  
    1.21 @@ -108,7 +108,7 @@
    1.22  	        val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
    1.23  	        val spec = (dI, pI, mI)
    1.24  	        val (pt,_) = 
    1.25 -		        Ctree.cappend_problem Ctree.e_ctree [] (Selem.e_istate, Ctree.e_ctxt) ([], e_spec) ([], e_spec, hdt)
    1.26 +		        Ctree.cappend_problem Ctree.e_ctree [] (Selem.e_istate, Selem.e_ctxt) ([], e_spec) ([], e_spec, hdt)
    1.27  	        val pt = Ctree.update_spec pt [] spec
    1.28  	        val pt = Ctree.update_pbl pt [] pits
    1.29  	        val pt = Ctree.update_met pt [] mits
    1.30 @@ -339,11 +339,11 @@
    1.31  fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) = 
    1.32        (Ctree.Rewrite (id, thm), 
    1.33           Ctree.Rewrite' ("Isac", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
    1.34 -       (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Selem.Uistate, Ctree.e_ctxt)))
    1.35 +       (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Selem.Uistate, Selem.e_ctxt)))
    1.36    | mk_tacis _ _ (t, r as Rls_ rls, (t', a)) = 
    1.37        (Ctree.Rewrite_Set (Lucin.rule2rls' r), 
    1.38           Ctree.Rewrite_Set' ("Isac", false, rls, t, (t', a)),
    1.39 -       (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Selem.Uistate, Ctree.e_ctxt)))
    1.40 +       (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Selem.Uistate, Selem.e_ctxt)))
    1.41    | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ rule2str r ^ " at " ^ term2str t)
    1.42  
    1.43  (* fo = ifo excluded already in inform *)
    1.44 @@ -403,7 +403,7 @@
    1.45                   val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)
    1.46  				         val mI = Ctree.get_obj Ctree.g_metID pt p
    1.47  			         in
    1.48 -			           Solve.nxt_solv (Ctree.Apply_Method' (mI, NONE, Selem.e_istate, Ctree.e_ctxt)) (Selem.e_istate, Ctree.e_ctxt) ptp
    1.49 +			           Solve.nxt_solv (Ctree.Apply_Method' (mI, NONE, Selem.e_istate, Selem.e_ctxt)) (Selem.e_istate, Selem.e_ctxt) ptp
    1.50                 end
    1.51  			     | _ => cs';
    1.52  		     in compare_step (tacis, c @ c' @ c'', ptp) ifo end