Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/function_package/size.ML
changeset 30345 76fd85bbf139
parent 30280 eb98b49ef835
child 30364 577edc39b501 
--- a/src/HOL/Tools/function_package/size.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -140,7 +140,7 @@
     val ((size_def_thms, size_def_thms'), thy') =
       thy
       |> Sign.add_consts_i (map (fn (s, T) =>
-           (NameSpace.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
+           (Binding.name (NameSpace.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
            (size_names ~~ recTs1))
       |> PureThy.add_defs false
         (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
isabelle