equal
deleted
inserted
replaced
382 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
382 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
383 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
383 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
384 val fv_names_all = fv_names_fst @ fv_bn_names; |
384 val fv_names_all = fv_names_fst @ fv_bn_names; |
385 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
385 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
386 (* Function_Fun.add_fun Function_Common.default_config ... true *) |
386 (* Function_Fun.add_fun Function_Common.default_config ... true *) |
387 val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all) |
387 (* val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)*) |
388 val (fvs, lthy') = (Primrec.add_primrec |
388 val (fvs, lthy') = (Primrec.add_primrec |
389 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) |
389 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) |
390 val (fvs2, lthy'') = |
390 val (fvs2, lthy'') = |
391 if fv_eqs_snd = [] then (([], []), lthy') else |
391 if fv_eqs_snd = [] then (([], []), lthy') else |
392 (Primrec.add_primrec |
392 (Primrec.add_primrec |