changeset 67522 | 9e712280cc37 |
parent 67405 | e9ab4ad7bd15 |
child 69597 | ff784d5a5bfb |
--- a/src/HOL/Nominal/nominal_inductive2.ML Sun Jan 28 16:09:00 2018 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sun Jan 28 19:28:52 2018 +0100 @@ -330,7 +330,7 @@ rotate_tac 1 1, REPEAT (eresolve_tac ctxt' [conjE] 1)]) [] ctxt; - val (Ts1, _ :: Ts2) = take_prefix (not o equal T) (map snd sets); + val (Ts1, _ :: Ts2) = chop_prefix (not o equal T) (map snd sets); val pTs = map NominalAtoms.mk_permT (Ts1 @ Ts2); val (pis1, pis2) = chop (length Ts1) (map Bound (length pTs - 1 downto 0));