src/Pure/tactic.ML
changeset 2228 f381c1a98209
parent 2145 5e8db0bc195e
child 2580 e3f680709487
     1.1 --- a/src/Pure/tactic.ML	Tue Nov 26 16:15:50 1996 +0100
     1.2 +++ b/src/Pure/tactic.ML	Tue Nov 26 16:18:42 1996 +0100
     1.3 @@ -352,7 +352,7 @@
     1.4        else    x :: untaglist rest;
     1.5  
     1.6  (*return list elements in original order*)
     1.7 -val orderlist = untaglist o sort (fn(x,y)=> #1 x < #1 y); 
     1.8 +fun orderlist kbrls = untaglist (sort (fn(x,y)=> #1 x < #1 y) kbrls); 
     1.9  
    1.10  (*insert one tagged brl into the pair of nets*)
    1.11  fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =