# HG changeset patch
# User wenzelm
# Date 1333440281 -7200
# Node ID ca4cf5de366c2b099b1793516ce08821f488edea
# Parent  0e65b6a016dc592eac80a8ffcf7aa23a66ee2e71
avoid const_declaration in aux. context (cf. locale_foundation);

diff -r 0e65b6a016dc -r ca4cf5de366c src/Pure/Isar/generic_target.ML
--- 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) #>