changeset 41489 | 8e2b8649507d |
parent 39557 | fe5722fce758 |
child 42364 | 8c674b3b8e44 |
--- a/src/HOL/Nominal/nominal_permeq.ML Mon Jan 10 08:18:49 2011 +0100 +++ b/src/HOL/Nominal/nominal_permeq.ML Mon Jan 10 15:19:48 2011 +0100 @@ -302,7 +302,7 @@ vs HOLogic.unit; val s' = list_abs (ps, Const ("Nominal.supp", fastype_of1 (Ts, s) --> - snd (split_last (binder_types T)) --> HOLogic.boolT) $ s); + List.last (binder_types T) --> HOLogic.boolT) $ s); val supports_rule' = Thm.lift_rule goal supports_rule; val _ $ (_ $ S $ _) = Logic.strip_assums_concl (hd (prems_of supports_rule'));