test/Tools/isac/Test_Some.thy
branchdecompose-isar
changeset 42282 80ad50a9e541
parent 42281 19d9ab32a0ce
child 42283 b95f0dde56c1
     1.1 --- a/test/Tools/isac/Test_Some.thy	Fri Sep 23 08:30:35 2011 +0200
     1.2 +++ b/test/Tools/isac/Test_Some.thy	Fri Sep 23 09:41:11 2011 +0200
     1.3 @@ -125,18 +125,6 @@
     1.4  ML {*
     1.5  *}
     1.6  ML {*
     1.7 -(*
     1.8 -assy ya ((E , l@[L,R], a,v,S,b),ss) e
     1.9 -(assy ((ts,d),Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
    1.10 -locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt')
    1.11 -solve m (pt, pos);
    1.12 -loc_solve_ (mI,m) ptp
    1.13 -locatetac tac (pt,p)
    1.14 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
    1.15 -WAS exception PTREE "get_obj: pos = [0] does not exist" 
    1.16 -raised (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")
    1.17 -*)
    1.18 -
    1.19  
    1.20  *}
    1.21  ML {*
    1.22 @@ -147,6 +135,7 @@
    1.23  ML{*
    1.24  *}
    1.25  ML {* (*=================*)
    1.26 +
    1.27  *}
    1.28  ML{*
    1.29  "~~~~~ fun , args:"; val () = ();