src/Pure/Isar/specification.ML
changeset 45584 41a768a431a6
parent 45583 93499f36d59a
child 45600 1bbbac9a0cb0
equal deleted inserted replaced
45583:93499f36d59a 45584:41a768a431a6
   373     val ((more_atts, prems, stmt, facts), goal_ctxt) =
   373     val ((more_atts, prems, stmt, facts), goal_ctxt) =
   374       prep_statement attrib prep_stmt elems raw_concl lthy;
   374       prep_statement attrib prep_stmt elems raw_concl lthy;
   375     val atts = more_atts @ map attrib raw_atts;
   375     val atts = more_atts @ map attrib raw_atts;
   376 
   376 
   377     fun after_qed' results goal_ctxt' =
   377     fun after_qed' results goal_ctxt' =
   378       let val results' =
   378       let
   379         burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results
   379         val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results;
   380       in
   380         val (res, lthy') =
   381         lthy
   381           if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy)
   382         |> Local_Theory.notes_kind kind
   382           else
   383           (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
   383             Local_Theory.notes_kind kind
   384         |> (fn (res, lthy') =>
   384               (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
   385           if Binding.is_empty name andalso null atts then
   385         val lthy'' =
       
   386           if Attrib.is_empty_binding (name, atts) then
   386             (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
   387             (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
   387           else
   388           else
   388             let
   389             let
   389               val ([(res_name, _)], lthy'') = lthy'
   390               val ([(res_name, _)], lthy'') =
   390                 |> Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])];
   391                 Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
   391               val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
   392               val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
   392             in lthy'' end)
   393             in lthy'' end;
   393         |> after_qed results'
   394       in after_qed results' lthy'' end;
   394       end;
       
   395   in
   395   in
   396     goal_ctxt
   396     goal_ctxt
   397     |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
   397     |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
   398     |> snd
   398     |> snd
   399     |> Proof.theorem before_qed after_qed' (map snd stmt)
   399     |> Proof.theorem before_qed after_qed' (map snd stmt)