--- 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;