1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Mon May 04 09:25:51 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Mon May 04 10:19:16 2020 +0200
     1.3 @@ -12,6 +12,8 @@
     1.4    val add_general: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
     1.5    val s_add_general: State_Steps.T ->
     1.6      Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
     1.7 +  val add_hard:
     1.8 +    theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Generate.test_out
     1.9  
    1.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.11    (*NONE*)                                                     
    1.12 @@ -297,18 +299,27 @@
    1.13  (* LI switches between solve-phase and specify-phase *)
    1.14  fun add_general tac ic cs =
    1.15    if Tactic.for_specify' tac
    1.16 -  then Generate.generate1 tac ic cs
    1.17 +  then Specify_Step.add tac ic cs
    1.18    else add tac ic cs
    1.19  
    1.20 -(* tacis are in reverse order from do_next/specify_: last = fst to insert *)
    1.21 +(* the order of State_Steps is reversed: insert last element first  *)
    1.22  fun s_add_general [] ptp = ptp
    1.23    | s_add_general tacis (pt, c, _) = 
    1.24      let
    1.25        val (tacis', (_, tac_, (p, is))) = split_last tacis
    1.26 -	    val (p',c',_,pt') = add_general tac_ is (pt, p)
    1.27 +	    val (p', c', _, pt') = add_general tac_ is (pt, p)
    1.28      in
    1.29        s_add_general tacis' (pt', c@c', p')
    1.30      end
    1.31  
    1.32 +(* a still undeveloped concept: do a calculation without LI *)
    1.33 +fun add_hard _(*thy*) m' (p, p_) pt =
    1.34 +  let  
    1.35 +    val p = case p_ of
    1.36 +      Pos.Frm => p | Pos.Res => Pos.lev_on p
    1.37 +    | _ => error ("generate_hard: call by " ^ Pos.pos'2str (p,p_))
    1.38 +  in
    1.39 +    add_general m' (Istate_Def.empty, ContextC.empty) (pt, (p, p_))
    1.40 +  end
    1.41  
    1.42  (**)end(**);