1.1 --- a/src/Tools/isac/Interpret/script.sml Fri Jul 15 13:51:50 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Jul 18 09:29:17 2011 +0200
1.3 @@ -348,14 +348,6 @@
1.4 *)
1.5
1.6
1.7 -(*["BOOL (1+x=2)","REAL x"] --match_ags--> oris
1.8 - --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"]*)
1.9 -fun oris2fmz_vals oris =
1.10 - let fun ori2fmz_vals ((_,_,_,dsc,ts):ori) =
1.11 - ((term2str o comp_dts') (dsc, ts), last_elem ts)
1.12 - handle _ => error ("ori2fmz_env called with "^terms2str ts)
1.13 - in (split_list o (map ori2fmz_vals)) oris end;
1.14 -
1.15 (*detour necessary, because generate1 delivers a string-result*)
1.16 fun mout2term thy (Form' (FormKF (_,_,_,_,res))) =
1.17 (term_of o the o (parse (assoc_thy thy))) res
1.18 @@ -908,7 +900,7 @@
1.19 (*this constructions doesnt allow arbitrary nesting of Or !!!*)
1.20
1.21
1.22 -(*assy, ass_up, astep_up scanning for locate_gen at stactic in a script.
1.23 +(*assy, ass_up, astep_up scan for locate_gen in a script.
1.24 search is clearly separated into (1)-(2):
1.25 (1) assy is recursive descent;
1.26 (2) ass_up resumes interpretation at a location somewhere in the script;