changeset 44692 | ccfc7c193d2b |
parent 43278 | 1fbdcebb364b |
child 44693 | a9635943a3e9 |
--- a/src/HOL/Nominal/nominal_permeq.ML Sat Sep 03 14:33:45 2011 -0700 +++ b/src/HOL/Nominal/nominal_permeq.ML Sat Sep 03 14:52:40 2011 -0700 @@ -303,7 +303,7 @@ vs HOLogic.unit; val s' = list_abs (ps, Const ("Nominal.supp", fastype_of1 (Ts, s) --> - List.last (binder_types T) --> HOLogic.boolT) $ s); + Term.range_type T) $ s); val supports_rule' = Thm.lift_rule goal supports_rule; val _ $ (_ $ S $ _) = Logic.strip_assums_concl (hd (prems_of supports_rule'));