src/Tools/isac/Interpret/solve.sml
branchdecompose-isar
changeset 42281 19d9ab32a0ce
parent 42092 1a6d6089e594
child 52153 26f274076fd2
     1.1 --- a/src/Tools/isac/Interpret/solve.sml	Thu Sep 22 14:43:47 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Fri Sep 23 08:30:35 2011 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4                val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
     1.5  	            val d = e_rls (*FIXME: get simplifier from domID*);
     1.6  	          in 
     1.7 -	            case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt') of 
     1.8 +	            case locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of 
     1.9  		            Steps (is'', ss as (m'',f',pt',p',c')::_) =>
    1.10  		              ("ok", (map step2taci ss, c', (pt',p')))
    1.11  		          | NotLocatable =>