1.1 --- a/src/Tools/isac/Interpret/appl.sml	Fri Apr 15 15:58:52 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Fri Apr 15 17:07:34 2011 +0200
     1.3 @@ -93,7 +93,7 @@
     1.4    | mk_set thy pt p (Const ("Tools.UniversalList",_)) pred =
     1.5      (e_term, if pred <> Const ("Script.Assumptions",bool)
     1.6  	     then [pred] 
     1.7 -	     else (map fst) (get_assumptions_ pt (p,Res)))
     1.8 +	     else get_assumptions_ pt (p,Res))
     1.9  
    1.10  (* val pred = (term_of o the o (parse thy)) pred;
    1.11     val consts as Const ("List.list.Cons",_) $ eq $ _ = ft;
    1.12 @@ -103,7 +103,7 @@
    1.13    let val (bdv,_) = HOLogic.dest_eq eq;
    1.14      val pred = if pred <> Const ("Script.Assumptions",bool)
    1.15  		 then [pred] 
    1.16 -	       else (map fst) (get_assumptions_ pt (p,Res))
    1.17 +	       else get_assumptions_ pt (p,Res)
    1.18    in (bdv, pred) end
    1.19  
    1.20    | mk_set thy _ _ l _ =