equal
deleted
inserted
replaced
722 (case (get_clauses thy s, get_assoc_code thy (s, T)) of |
722 (case (get_clauses thy s, get_assoc_code thy (s, T)) of |
723 (SOME (names, thyname, k, intrs), NONE) => |
723 (SOME (names, thyname, k, intrs), NONE) => |
724 let |
724 let |
725 val (ts1, ts2) = chop k ts; |
725 val (ts1, ts2) = chop k ts; |
726 val ts2' = map |
726 val ts2' = map |
727 (fn Bound i => Term.dummy_pattern (nth Ts i) | t => t) ts2; |
727 (fn Bound i => Term.dummy_pattern (nth Ts (length Ts - i - 1)) | t => t) ts2; |
728 val (ots, its) = List.partition is_Bound ts2; |
728 val (ots, its) = List.partition is_Bound ts2; |
729 val no_loose = forall (fn t => not (loose_bvar (t, 0))) |
729 val no_loose = forall (fn t => not (loose_bvar (t, 0))) |
730 in |
730 in |
731 if null (duplicates op = ots) andalso |
731 if null (duplicates op = ots) andalso |
732 no_loose ts1 andalso no_loose its |
732 no_loose ts1 andalso no_loose its |