src/Pure/Isar/expression.ML
changeset 35798 fd1bb29f8170
parent 35625 9c818cab0dd0
child 35845 e5980f0ad025
     1.1 --- a/src/Pure/Isar/expression.ML	Mon Mar 15 15:13:22 2010 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Mon Mar 15 18:59:16 2010 +0100
     1.3 @@ -772,7 +772,7 @@
     1.4  
     1.5      val loc_ctxt = thy'
     1.6        |> Locale.register_locale binding (extraTs, params)
     1.7 -          (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
     1.8 +          (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
     1.9        |> Theory_Target.init (SOME name)
    1.10        |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
    1.11