1.1 --- a/src/Pure/Isar/generic_target.ML	Tue Apr 03 09:47:20 2012 +0200
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 10:04:41 2012 +0200
     1.3 @@ -287,8 +287,10 @@
     1.4  
     1.5  fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
     1.6    background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
     1.7 -  #-> (fn (lhs, def) => const_declaration (K true) Syntax.mode_default ((b, mx), lhs)
     1.8 -    #> pair (lhs, def));
     1.9 +  #-> (fn (lhs, def) => fn lthy' => lthy' |>
    1.10 +        const_declaration (fn level => level <> Local_Theory.level lthy')
    1.11 +          Syntax.mode_default ((b, mx), lhs)
    1.12 +    |> pair (lhs, def));
    1.13  
    1.14  fun theory_notes kind global_facts local_facts =
    1.15    Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>