src/Tools/isac/Interpret/solve.sml
branchdecompose-isar
changeset 41957 703d656a6291
parent 41953 63c956fc503e
child 41959 a0d6a7c3e1df
     1.1 --- a/src/Tools/isac/Interpret/solve.sml	Fri Apr 15 15:58:52 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Fri Apr 15 17:07:34 2011 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4        val asm = (case get_obj g_tac pt p of
     1.5  		    Check_elementwise _ => (*collects and instantiates asms*)
     1.6  		    (snd o (get_obj g_result pt)) p
     1.7 -		  | _ => ((map fst) o (get_assumptions_ pt)) (p,p_))
     1.8 +		  | _ => get_assumptions_ pt (p,p_))
     1.9  	  handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
    1.10        val metID = get_obj g_metID pt pp;
    1.11        val {srls=srls,scr=sc,...} = get_met metID;
    1.12 @@ -356,7 +356,7 @@
    1.13        val asm = (case get_obj g_tac pt p of
    1.14  		    Check_elementwise _ => (*collects and instantiates asms*)
    1.15  		    (snd o (get_obj g_result pt)) p
    1.16 -		  | _ => ((map fst) o (get_assumptions_ pt)) (p,p_))
    1.17 +		  | _ => get_assumptions_ pt (p,p_))
    1.18  	  handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
    1.19        val metID = get_obj g_metID pt pp;
    1.20        val {srls=srls,scr=sc,...} = get_met metID;