equal
deleted
inserted
replaced
1941 ^ Syntax.string_of_typ ctxt (Type (s', Ts')) |
1941 ^ Syntax.string_of_typ ctxt (Type (s', Ts')) |
1942 ^ ") is not a variable") |
1942 ^ ") is not a variable") |
1943 else () |
1943 else () |
1944 (* split the constructors into those occurring before/after *) |
1944 (* split the constructors into those occurring before/after *) |
1945 (* 'Const (s, T)' *) |
1945 (* 'Const (s, T)' *) |
1946 val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) => |
1946 val (constrs1, constrs2) = chop_prefix (fn (cname, ctypes) => |
1947 not (cname = s andalso Sign.typ_instance thy (T, |
1947 not (cname = s andalso Sign.typ_instance thy (T, |
1948 map (typ_of_dtyp descr typ_assoc) ctypes |
1948 map (typ_of_dtyp descr typ_assoc) ctypes |
1949 ---> Type (s', Ts')))) constrs |
1949 ---> Type (s', Ts')))) constrs |
1950 in |
1950 in |
1951 case constrs2 of |
1951 case constrs2 of |
2654 (assoc, (offsets, off + 1)) |
2654 (assoc, (offsets, off + 1)) |
2655 else |
2655 else |
2656 (* go back up the stack until we find a level where we can go *) |
2656 (* go back up the stack until we find a level where we can go *) |
2657 (* to the next sibling node *) |
2657 (* to the next sibling node *) |
2658 let |
2658 let |
2659 val offsets' = snd (take_prefix |
2659 val offsets' = drop_prefix (fn off' => off' mod size_elem = size_elem - 1) offsets |
2660 (fn off' => off' mod size_elem = size_elem - 1) offsets) |
|
2661 in |
2660 in |
2662 case offsets' of |
2661 case offsets' of |
2663 [] => |
2662 [] => |
2664 (* we're at the last node in the tree; the next value *) |
2663 (* we're at the last node in the tree; the next value *) |
2665 (* won't be used anyway *) |
2664 (* won't be used anyway *) |