| changeset 37391 | 476270a6c2dc |
| parent 36960 | 01594f816e3a |
| child 37677 | c5a8b612e571 |
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Jun 10 12:24:02 2010 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Thu Jun 10 12:24:03 2010 +0200 @@ -121,7 +121,7 @@ val dj_cp = thm "dj_cp"; -fun dest_permT (Type ("fun", [Type ("List.list", [Type ("*", [T, _])]), +fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [T, _])]), Type ("fun", [_, U])])) = (T, U); fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u