src/Pure/Isar/specification.ML

 
 (* complex goal statements *)
 
 local
 
+fun subtract_prems ctxt1 ctxt2 =
+  Library.drop (length (Assumption.prems_of ctxt1), Assumption.prems_of ctxt2);
+
 fun prep_statement prep_att prep_stmt elems concl ctxt =
   (case concl of
     Element.Shows shows =>
       let
-        val (_, _, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt;
+        val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt;
+        val prems = subtract_prems loc_ctxt elems_ctxt;
+        val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
         val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
-        val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
-      in ((stmt, []), goal_ctxt) end
+      in ((prems, stmt, []), goal_ctxt) end
   | Element.Obtains obtains =>
       let
         val case_names = obtains |> map_index
           (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
         val constraints = obtains |> map (fn (_, (vars, _)) =>
           Locale.Elem (Element.Constrains
             (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE))));
 
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
-        val (_, _, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
+        val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
 
         val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
 
         fun assume_case ((name, (vars, _)), asms) ctxt' =
           let

             |>> (fn [(_, [th])] => th)
           end;
 
         val atts = map Attrib.internal
           [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
+        val prems = subtract_prems loc_ctxt elems_ctxt;
         val stmt = [(("", atts), [(thesis, [])])];
 
         val (facts, goal_ctxt) = elems_ctxt
           |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
           |> fold_map assume_case (obtains ~~ propp)
           |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
                 [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
-      in ((stmt, facts), goal_ctxt) end);
+      in ((prems, stmt, facts), goal_ctxt) end);
 
 fun gen_theorem prep_att prep_stmt
     kind before_qed after_qed (name, raw_atts) raw_elems raw_concl lthy0 =
   let
     val _ = LocalTheory.assert lthy0;

     val attrib = prep_att thy;
     val atts = map attrib raw_atts;
 
     val elems = raw_elems |> (map o Locale.map_elem)
       (Element.map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib});
-    val ((stmt, facts), goal_ctxt) = prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
+    val ((prems, stmt, facts), goal_ctxt) =
+      prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
 
     fun after_qed' results goal_ctxt' =
       let val results' = burrow (ProofContext.export_standard goal_ctxt' lthy) results in
         lthy
         |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')

             else #2 (LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])] lthy')))
         |> after_qed results'
       end;
   in
     goal_ctxt
+    |> ProofContext.note_thmss_i Thm.assumptionK [((AutoBind.assmsN, []), [(prems, [])])]
+    |> snd
     |> Proof.theorem_i before_qed after_qed' (map snd stmt)
     |> Proof.refine_insert facts
   end;
 
 in