let

   let

     val eqns = List.concat blocks;

     val eqns = List.concat blocks;

     val lengths = map length blocks;

     val lengths = map length blocks;

     val ((bindings, srcss), strings) = apfst split_list (split_list eqns);

     val ((bindings, srcss), strings) = apfst split_list (split_list eqns);

     val atts = map (map (prep_attrib thy)) srcss;

     val atts = map (map (prep_attrib thy)) srcss;

     val eqn_ts = map (prep_prop thy) strings;

     val eqn_ts = map (prep_prop thy) strings;

     val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq)))

     val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq)))

       handle TERM _ => fixrec_eq_err thy "not a proper equation" eq) eqn_ts;

       handle TERM _ => fixrec_eq_err thy "not a proper equation" eq) eqn_ts;

     val (_, eqn_ts') = OldPrimrecPackage.unify_consts thy rec_ts eqn_ts;

     val (_, eqn_ts') = OldPrimrecPackage.unify_consts thy rec_ts eqn_ts;

   let

   let

     val atts = map (prep_attrib thy) srcs;

     val atts = map (prep_attrib thy) srcs;

     val ts = map (prep_term thy) strings;

     val ts = map (prep_term thy) strings;

     val simps = map (fix_pat thy) ts;

     val simps = map (fix_pat thy) ts;

   in

   in

   end;

   end;

 val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;

 val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;

 val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I);

 val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I);