src/HOL/Tools/function_package/size.ML
changeset 25017 e82ab4962f80
parent 24962 60d33fb8ea5d
child 25155 65612c9f7381
     1.1 --- a/src/HOL/Tools/function_package/size.ML	Sat Oct 13 17:16:39 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/size.ML	Sat Oct 13 17:16:40 2007 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4        (map (fn T => name_of_typ T ^ size_suffix) (Library.drop (head_len, recTs)));
     1.5  
     1.6      val thy' = thy |> fold (fn (s, T) =>
     1.7 -        snd o Theory.specify_const [] (Sign.base_name s, T --> HOLogic.natT, NoSyn))
     1.8 +        snd o Theory.specify_const [] (Sign.base_name s, T --> HOLogic.natT, NoSyn) [])
     1.9        (size_names ~~ Library.drop (head_len, recTs))
    1.10      val size_axs = make_size head_len descr' sorts recTs thy';
    1.11    in