src/Pure/Isar/expression.ML
changeset 59296 002d817b4c37
parent 58956 a816aa3ff391
child 59573 d09cc83cdce9
     1.1 --- a/src/Pure/Isar/expression.ML	Mon Jan 05 23:33:39 2015 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Mon Jan 05 18:39:32 2015 +0100
     1.3 @@ -762,6 +762,10 @@
     1.4            [(Attrib.internal o K) Locale.witness_add])])) defs)
     1.5    | defines_to_notes _ e = e;
     1.6  
     1.7 +fun is_hyp (elem as Assumes asms) = true
     1.8 +  | is_hyp (elem as Defines defs) = true
     1.9 +  | is_hyp _ = false;
    1.10 +
    1.11  fun gen_add_locale prep_decl
    1.12      binding raw_predicate_binding raw_import raw_body thy =
    1.13    let
    1.14 @@ -798,6 +802,8 @@
    1.15          map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems;
    1.16      val asm = if is_some b_statement then b_statement else a_statement;
    1.17  
    1.18 +    val hyp_spec = filter is_hyp body_elems;
    1.19 +
    1.20      val notes =
    1.21        if is_some asm then
    1.22          [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
    1.23 @@ -820,7 +826,7 @@
    1.24  
    1.25      val loc_ctxt = thy'
    1.26        |> Locale.register_locale binding (extraTs, params)
    1.27 -          (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
    1.28 +          (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps')
    1.29        |> Named_Target.init name
    1.30        |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
    1.31