src/Tools/isac/Interpret/script.sml
branchdecompose-isar
changeset 42092 1a6d6089e594
parent 42082 2556b7865f9b
child 42133 f9a7294e6cd6
     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;