changeset 30364 | 577edc39b501 |
parent 30280 | eb98b49ef835 |
child 31723 | f5cafe803b55 |
--- a/src/HOL/Tools/TFL/tfl.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/TFL/tfl.ML Sun Mar 08 17:26:14 2009 +0100 @@ -349,7 +349,7 @@ | L => mk_functional_err ("The following clauses are redundant (covered by preceding clauses): " ^ commas (map (fn i => Int.toString (i + 1)) L)) - in {functional = Abs(NameSpace.base_name fname, ftype, + in {functional = Abs(Long_Name.base_name fname, ftype, abstract_over (atom, absfree(aname,atype, case_tm))), pats = patts2}