1.1 --- a/src/Tools/isac/Interpret/solve.sml	Tue Oct 22 17:38:34 2013 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Thu Oct 24 00:02:29 2013 +0100
     1.3 @@ -424,10 +424,10 @@
     1.4    in complete_solve auto (c @ c') ptp end;
     1.5  
     1.6  (* aux.fun for detailrls with Rrls, reverse rewriting *)
     1.7 -fun rul_terms_2nds nds t [] = nds
     1.8 -  | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) =
     1.9 -    (append_atomic [] (e_istate, e_ctxt) t (rule2tac [] rule) res Complete EmptyPtree) ::
    1.10 -    (rul_terms_2nds nds t' rts);
    1.11 +fun rul_terms_2nds _ nds t [] = nds
    1.12 +  | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =
    1.13 +    (append_atomic [] (e_istate, e_ctxt) t (rule2tac thy [] rule) res Complete EmptyPtree) ::
    1.14 +    (rul_terms_2nds thy nds t' rts);
    1.15  
    1.16  (* detail steps done internally by Rewrite_Set* into ctree by use of a script *)
    1.17  fun detailrls pt (pos as (p,p_):pos') = 
    1.18 @@ -441,7 +441,7 @@
    1.19  	    Rrls {scr = Rfuns {init_state,...},...} => 
    1.20  	      let
    1.21            val (_,_,_,rul_terms) = init_state t
    1.22 -	        val newnds = rul_terms_2nds [] t rul_terms
    1.23 +	        val newnds = rul_terms_2nds (Proof_Context.theory_of ctxt) [] t rul_terms
    1.24  	        val pt''' = ins_chn newnds pt p 
    1.25  	      in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
    1.26  	  | _ =>