equal
deleted
inserted
replaced
229 val ((names, srcss), strings) = apfst split_list (split_list eqns); |
229 val ((names, srcss), strings) = apfst split_list (split_list eqns); |
230 val atts = map (map (prep_attrib thy)) srcss; |
230 val atts = map (map (prep_attrib thy)) srcss; |
231 val eqn_ts = map (prep_prop thy) strings; |
231 val eqn_ts = map (prep_prop thy) strings; |
232 val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq))) |
232 val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq))) |
233 handle TERM _ => fixrec_eq_err thy "not a proper equation" eq) eqn_ts; |
233 handle TERM _ => fixrec_eq_err thy "not a proper equation" eq) eqn_ts; |
234 val (_, eqn_ts') = PrimrecPackage.unify_consts thy rec_ts eqn_ts; |
234 val (_, eqn_ts') = OldPrimrecPackage.unify_consts thy rec_ts eqn_ts; |
235 |
235 |
236 fun unconcat [] _ = [] |
236 fun unconcat [] _ = [] |
237 | unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n)); |
237 | unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n)); |
238 val pattern_blocks = unconcat lengths (map Logic.strip_imp_concl eqn_ts'); |
238 val pattern_blocks = unconcat lengths (map Logic.strip_imp_concl eqn_ts'); |
239 val compiled_ts = map (legacy_infer_term thy o compile_pats) pattern_blocks; |
239 val compiled_ts = map (legacy_infer_term thy o compile_pats) pattern_blocks; |