src/Pure/sign.ML
changeset 42376 c3abf2c3f541
parent 42375 774df7c59508
child 42381 309ec68442c6
     1.1 --- a/src/Pure/sign.ML	Sun Apr 17 19:54:04 2011 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Apr 17 20:15:46 2011 +0200
     1.3 @@ -419,13 +419,7 @@
     1.4  fun add_consts_i args thy =
     1.5    #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
     1.6  
     1.7 -fun declare_const ctxt ((b, T), mx) thy =
     1.8 -  let
     1.9 -    val pos = Binding.pos_of b;
    1.10 -    val ([const as Const (c, _)], thy') = gen_add_consts (K I) ctxt [(b, T, mx)] thy;
    1.11 -    val _ = Position.report pos (Markup.const_decl c);
    1.12 -  in (const, thy') end;
    1.13 -
    1.14 +fun declare_const ctxt ((b, T), mx) = yield_singleton (gen_add_consts (K I) ctxt) (b, T, mx);
    1.15  fun declare_const_global arg thy = declare_const (Proof_Context.init_global thy) arg thy;
    1.16  
    1.17  end;