changeset 2228 | f381c1a98209 |
parent 2145 | 5e8db0bc195e |
child 2580 | e3f680709487 |
--- a/src/Pure/tactic.ML Tue Nov 26 16:15:50 1996 +0100 +++ b/src/Pure/tactic.ML Tue Nov 26 16:18:42 1996 +0100 @@ -352,7 +352,7 @@ 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)) =