1.1 --- a/src/Pure/Isar/generic_target.ML	Tue Apr 03 09:41:16 2012 +0200
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 09:47:20 2012 +0200
     1.3 @@ -30,6 +30,8 @@
     1.4      Context.generic -> Context.generic
     1.5    val const_declaration: (int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
     1.6      local_theory -> local_theory
     1.7 +  val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     1.8 +    term list * term list -> local_theory -> (term * thm) * local_theory
     1.9    val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
    1.10      term list * term list -> local_theory -> (term * thm) * local_theory
    1.11    val theory_notes: string ->
    1.12 @@ -272,7 +274,7 @@
    1.13  
    1.14  (** primitive theory operations **)
    1.15  
    1.16 -fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    1.17 +fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    1.18    let
    1.19      val (const, lthy2) = lthy
    1.20        |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx));
    1.21 @@ -283,6 +285,11 @@
    1.22            (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
    1.23    in ((lhs, def), lthy3) end;
    1.24  
    1.25 +fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    1.26 +  background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
    1.27 +  #-> (fn (lhs, def) => const_declaration (K true) Syntax.mode_default ((b, mx), lhs)
    1.28 +    #> pair (lhs, def));
    1.29 +
    1.30  fun theory_notes kind global_facts local_facts =
    1.31    Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
    1.32    (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt =>

     2.1 --- a/src/Pure/Isar/named_target.ML	Tue Apr 03 09:41:16 2012 +0200
     2.2 +++ b/src/Pure/Isar/named_target.ML	Tue Apr 03 09:47:20 2012 +0200
     2.3 @@ -70,19 +70,14 @@
     2.4  
     2.5  (* define *)
     2.6  
     2.7 -fun global_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
     2.8 -  Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
     2.9 -  #-> (fn (lhs, def) => Generic_Target.const_declaration (K true) Syntax.mode_default ((b, mx), lhs)
    2.10 -    #> pair (lhs, def));
    2.11 -
    2.12  fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    2.13 -  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    2.14 +  Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    2.15    #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs)
    2.16      #> pair (lhs, def));
    2.17  
    2.18  fun class_foundation (ta as Target {target, ...})
    2.19      (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    2.20 -  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    2.21 +  Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    2.22    #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs)
    2.23      #> Class.const target ((b, mx), (type_params, lhs))
    2.24      #> pair (lhs, def));
    2.25 @@ -90,7 +85,7 @@
    2.26  fun target_foundation (ta as Target {is_locale, is_class, ...}) =
    2.27    if is_class then class_foundation ta
    2.28    else if is_locale then locale_foundation ta
    2.29 -  else global_foundation;
    2.30 +  else Generic_Target.theory_foundation;
    2.31  
    2.32  
    2.33  (* notes *)