src/Pure/Isar/expression.ML
changeset 35021 c839a4c670c6
parent 33671 4b0f2599ed48
child 35143 7b2538c987e7
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Feb 07 19:31:55 2010 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Feb 07 19:33:34 2010 +0100
     1.3 @@ -699,7 +699,7 @@
     1.4              |> PureThy.note_thmss ""
     1.5                   [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
     1.6                    ((Binding.conceal (Binding.name axiomsN), []),
     1.7 -                    [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
     1.8 +                    [(map (Drule.export_without_context o Element.conclude_witness) axioms, [])])]
     1.9              ||> Sign.restore_naming thy''';
    1.10          in (SOME statement, SOME intro, axioms, thy'''') end;
    1.11    in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;