# HG changeset patch
# User wenzelm
# Date 1192111532 -7200
# Node ID 60d33fb8ea5d562fd1faeaa05b68a7019dc3e680
# Parent  5298ee9c3fe5ce9f403b825ec9df0abac95bc8f1
Theory.specify_const;

diff -r 5298ee9c3fe5 -r 60d33fb8ea5d src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Thu Oct 11 16:05:30 2007 +0200
+++ b/src/HOL/Tools/function_package/size.ML	Thu Oct 11 16:05:32 2007 +0200
@@ -25,16 +25,6 @@
   fun merge _ = Symtab.merge (K true);
 );
 
-fun specify_consts args thy =
-  let
-    val specs = map (fn (c, T, mx) =>
-      Const (Sign.full_name thy (Syntax.const_name c mx), T)) args;
-  in
-    thy
-    |> Sign.add_consts_authentic [] args
-    |> Theory.add_finals_i false specs
-  end;
-
 fun add_axioms label ts atts thy =
   thy
   |> PureThy.add_axiomss_i [((label, ts), atts)];
@@ -165,10 +155,9 @@
     val size_names = DatatypeProp.indexify_names
       (map (fn T => name_of_typ T ^ size_suffix) (Library.drop (head_len, recTs)));
 
-    val thy' = thy
-      |> specify_consts (map (fn (s, T) =>
-        (Sign.base_name s, T --> HOLogic.natT, NoSyn))
-          (size_names ~~ Library.drop (head_len, recTs)))
+    val thy' = thy |> fold (fn (s, T) =>
+        snd o Theory.specify_const [] (Sign.base_name s, T --> HOLogic.natT, NoSyn))
+      (size_names ~~ Library.drop (head_len, recTs))
     val size_axs = make_size head_len descr' sorts recTs thy';
   in
     thy'