# HG changeset patch
# User wenzelm
# Date 1572876414 -3600
# Node ID c9f5f724abc0a83bd321090f13eda0b857a38bfd
# Parent  d32ed8927a428a272533794a362dc69392133949
prefer named result;

diff -r d32ed8927a42 -r c9f5f724abc0 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Nov 04 14:56:49 2019 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Nov 04 15:06:54 2019 +0100
@@ -752,13 +752,13 @@
           val ((statement, intro, axioms), thy') =
             thy
             |> def_pred abinding parms defs' exts exts';
-          val (_, thy'') =
+          val ((_, [intro']), thy'') =
             thy'
             |> Sign.qualified_path true abinding
             |> Global_Theory.note_thms ""
               ((Binding.name introN, []), [([intro], [Locale.unfold_add])])
             ||> Sign.restore_naming thy';
-          in (SOME statement, SOME intro, axioms, thy'') end;
+          in (SOME statement, SOME intro', axioms, thy'') end;
     val (b_pred, b_intro, b_axioms, thy'''') =
       if null ints then (NONE, NONE, [], thy'')
       else
@@ -767,7 +767,7 @@
             thy''
             |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
           val ctxt''' = Proof_Context.init_global thy''';
-          val (_, thy'''') =
+          val ([(_, [intro']), _], thy'''') =
             thy'''
             |> Sign.qualified_path true binding
             |> Global_Theory.note_thmss ""
@@ -776,7 +776,7 @@
                     [(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms,
                       [])])]
             ||> Sign.restore_naming thy''';
-        in (SOME statement, SOME intro, axioms, thy'''') end;
+        in (SOME statement, SOME intro', axioms, thy'''') end;
   in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
 
 end;