# HG changeset patch
# User wenzelm
# Date 1144922466 -7200
# Node ID 43bfe55759b0b4620ee4623d287f62c9314f5a60
# Parent  f086002893adbba2700e75f31ec6237c98ebaea1
tuned;

diff -r f086002893ad -r 43bfe55759b0 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Apr 13 12:01:05 2006 +0200
+++ b/src/Pure/theory.ML	Thu Apr 13 12:01:06 2006 +0200
@@ -295,8 +295,8 @@
     fun const_of (Const const) = const
       | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
       | const_of _ = error "Attempt to finalize non-constant term";
-    fun specify (c, T) =
-      Defs.define (Sign.the_const_type thy) ((false, Context.theory_name thy), c ^ " axiom") (prep_const thy (c, T)) [];
+    fun specify (c, T) = Defs.define (Sign.the_const_type thy)
+      ((false, Context.theory_name thy), c ^ " axiom") (prep_const thy (c, T)) [];
     val finalize = specify o check_overloading thy overloaded o
       const_of o Sign.no_vars (Sign.pp thy) o prep_term thy;
   in thy |> map_defs (fold finalize args) end;