# HG changeset patch
# User wenzelm
# Date 1333439240 -7200
# Node ID 0e65b6a016dc592eac80a8ffcf7aa23a66ee2e71
# Parent  d344f6d9cc85e7261a5c14b979e5fa4166a7ab0c
clarified background_foundation vs. theory_foundation (with const_declaration);

diff -r d344f6d9cc85 -r 0e65b6a016dc src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Apr 03 09:41:16 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 09:47:20 2012 +0200
@@ -30,6 +30,8 @@
     Context.generic -> Context.generic
   val const_declaration: (int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
+  val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
+    term list * term list -> local_theory -> (term * thm) * local_theory
   val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
   val theory_notes: string ->
@@ -272,7 +274,7 @@
 
 (** primitive theory operations **)
 
-fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   let
     val (const, lthy2) = lthy
       |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx));
@@ -283,6 +285,11 @@
           (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
   in ((lhs, def), lthy3) end;
 
+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));
+
 fun theory_notes kind global_facts local_facts =
   Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
   (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt =>
diff -r d344f6d9cc85 -r 0e65b6a016dc src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Tue Apr 03 09:41:16 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Tue Apr 03 09:47:20 2012 +0200
@@ -70,19 +70,14 @@
 
 (* define *)
 
-fun global_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
-  Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
-  #-> (fn (lhs, def) => Generic_Target.const_declaration (K true) Syntax.mode_default ((b, mx), lhs)
-    #> pair (lhs, def));
-
 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
-  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
+  Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
   #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs)
     #> pair (lhs, def));
 
 fun class_foundation (ta as Target {target, ...})
     (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
-  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
+  Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
   #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs)
     #> Class.const target ((b, mx), (type_params, lhs))
     #> pair (lhs, def));
@@ -90,7 +85,7 @@
 fun target_foundation (ta as Target {is_locale, is_class, ...}) =
   if is_class then class_foundation ta
   else if is_locale then locale_foundation ta
-  else global_foundation;
+  else Generic_Target.theory_foundation;
 
 
 (* notes *)