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