1.1 --- a/src/Tools/isac/Interpret/generate.sml	Sun May 15 12:36:29 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Sun May 15 13:23:12 2011 +0200
     1.3 @@ -264,13 +264,14 @@
     1.4           case p_ of
     1.5             Pbl => update_pbl pt p itmlist
     1.6  	       | Met => update_met pt p itmlist)
     1.7 -
     1.8 +    (*WN110515 probably declare_constraints with input item (without dsc) --
     1.9 +      -- important when specifying without formalisation*)
    1.10    | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p,p_)) pt = 
    1.11        (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
    1.12           case p_ of
    1.13             Pbl => update_pbl pt p itmlist
    1.14  	       | Met => update_met pt p itmlist)
    1.15 -
    1.16 +    (*WN110515 probably declare_constraints with input item (without dsc)*)
    1.17    | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p,p_)) pt = 
    1.18        (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
    1.19           case p_ of
    1.20 @@ -483,38 +484,28 @@
    1.21        let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
    1.22  	      val (pt,c) =
    1.23            cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl);
    1.24 -        val pt = update_ctxt pt p ctxt (*FIXME.WN110511*)   
    1.25 +        val pt = update_ctxt pt p ctxt
    1.26  	      val f = Syntax.string_of_term (thy2ctxt thy) f;
    1.27        in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
    1.28  
    1.29    | generate1 thy m' _ _ _ = 
    1.30 -      error ("generate1: not impl.for "^(tac_2str m'))
    1.31 -;
    1.32 -
    1.33 +      error ("generate1: not impl.for "^(tac_2str m'));
    1.34  
    1.35  fun generate_hard thy m' (p,p_) pt =
    1.36    let  
    1.37 -    val p = case p_ of Frm => p | Res => lev_on p
    1.38 -  | _ => error ("generate_hard: call by "^(pos'2str (p,p_)));
    1.39 +    val p =
    1.40 +      case p_ of
    1.41 +        Frm => p | Res => lev_on p
    1.42 +      | _ => error ("generate_hard: call by " ^ pos'2str (p,p_));
    1.43    in generate1 thy m' (e_istate, e_ctxt) (p,p_) pt end;
    1.44  
    1.45 -
    1.46 -
    1.47  (*tacis are in reverse order from nxt_solve_/specify_: last = fst to insert*)
    1.48 -(* val (tacis, (pt, _)) = (tacis, ptp);
    1.49 -
    1.50 -   val (tacis, (pt, c, _)) = (rev tacis, (pt, [], (p, Res)));
    1.51 -   *)
    1.52  fun generate ([]: taci list) ptp = ptp
    1.53    | generate tacis (pt, c, _:pos'(*!dropped!WN0504redesign generate/tacis?*))= 
    1.54 -    let val (tacis', (_, tac_, (p, is))) = split_last tacis
    1.55 -	(* for recursion ...
    1.56 -	 (tacis', (_, tac_, (p, is))) = split_last tacis';
    1.57 -	 *)
    1.58 -	val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
    1.59 -    in generate tacis' (pt', c@c', p') end;
    1.60 -
    1.61 - 
    1.62 +      let
    1.63 +        val (tacis', (_, tac_, (p, is))) = split_last tacis
    1.64 +	      val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
    1.65 +      in generate tacis' (pt', c@c', p') end;
    1.66  
    1.67  (*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls       *
    1.68   *  of for connecting a user-input formula with the current calc-state.	     *