1.1 --- a/src/Tools/isac/MathEngine/solve.sml	Fri Mar 20 19:31:55 2020 +0100
     1.2 +++ b/src/Tools/isac/MathEngine/solve.sml	Mon Mar 23 13:31:29 2020 +0100
     1.3 @@ -14,7 +14,6 @@
     1.4    val complete_solve :
     1.5       auto -> Ctree.pos' list -> Calc.T -> string * Ctree.pos' list * Calc.T
     1.6  
     1.7 -  val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
     1.8  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     1.9    (*NONE*)
    1.10  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.11 @@ -93,39 +92,4 @@
    1.12        complete_solve auto (c @ c') ptp
    1.13      end;
    1.14  
    1.15 -(* aux.fun for detailrls with Rrls, reverse rewriting *)
    1.16 -fun rul_terms_2nds _ nds _ [] = nds
    1.17 -  | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =
    1.18 -    (append_atomic [] (NONE(*guessed*), (Istate.e_istate, ContextC.e_ctxt)) t (Tactic.rule2tac thy [] rule) res Complete EmptyPtree) ::
    1.19 -      (rul_terms_2nds thy nds t' rts);
    1.20 -
    1.21 -(* detail steps done internally by Rewrite_Set* into Ctree 
    1.22 -  by use of a program *)
    1.23 -fun detailrls pt (pos as (p, _)) = 
    1.24 -  let
    1.25 -    val t = get_obj g_form pt p
    1.26 -	  val tac = get_obj g_tac pt p
    1.27 -	  val rls = (assoc_rls o Tactic.rls_of) tac
    1.28 -    val ctxt = get_ctxt pt pos
    1.29 -  in
    1.30 -    case rls of
    1.31 -	    Rule.Rrls {scr = Rule.Rfuns {init_state, ...}, ...} => 
    1.32 -	    let
    1.33 -        val (_, _, _, rul_terms) = init_state t
    1.34 -	      val newnds = rul_terms_2nds (Proof_Context.theory_of ctxt) [] t rul_terms
    1.35 -	      val pt''' = ins_chn newnds pt p 
    1.36 -	    in ("detailrls", pt''', (p @ [length newnds], Res)) end
    1.37 -	  | _ =>
    1.38 -	    let
    1.39 -        val is = Generate.init_istate tac t
    1.40 -	      val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
    1.41 -	      val pos' = ((lev_on o lev_dn) p, Frm)
    1.42 -	      val thy = Celem.assoc_thy "Isac_Knowledge"
    1.43 -	      val (_, _, _, pt') = Generate.generate1 tac_ (is, ctxt) (pt, pos') (* implicit Take *)
    1.44 -	      val (_,_, (pt'', _)) = complete_solve CompleteSubpbl [] (pt', pos')
    1.45 -	      val newnds = children (get_nd pt'' p)
    1.46 -	      val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*)
    1.47 -	    in ("detailrls", pt''', (p @ [length newnds], Res)) end
    1.48 -  end;
    1.49 -
    1.50  end
    1.51 \ No newline at end of file