equal
deleted
inserted
replaced
74 in SOME (atom', maps mk_subst_rhs assms) end |
74 in SOME (atom', maps mk_subst_rhs assms) end |
75 |
75 |
76 fun flatten constname atom (defs, thy) = |
76 fun flatten constname atom (defs, thy) = |
77 if is_compound atom then |
77 if is_compound atom then |
78 let |
78 let |
79 val atom = Envir.beta_norm (Pattern.eta_long [] atom) |
79 val atom = Envir.beta_norm (Envir.eta_long [] atom) |
80 val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs)) |
80 val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs)) |
81 ((Long_Name.base_name constname) ^ "_aux") |
81 ((Long_Name.base_name constname) ^ "_aux") |
82 val full_constname = Sign.full_bname thy constname |
82 val full_constname = Sign.full_bname thy constname |
83 val (params, args) = List.partition (is_predT o fastype_of) |
83 val (params, args) = List.partition (is_predT o fastype_of) |
84 (map Free (Term.add_frees atom [])) |
84 (map Free (Term.add_frees atom [])) |