src/Pure/tactic.ML

   | untaglist ((k,x) :: (rest as (k',x')::_)) =
       if k=k' then untaglist rest
       else    x :: untaglist rest;
 
 (*return list elements in original order*)
-val orderlist = untaglist o sort (fn(x,y)=> #1 x < #1 y); 
+fun orderlist kbrls = untaglist (sort (fn(x,y)=> #1 x < #1 y) kbrls); 
 
 (*insert one tagged brl into the pair of nets*)
 fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
     if eres then 
 	case prems_of th of