src/HOL/Tools/TFL/tfl.ML
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}