src/Pure/Isar/specification.ML
changeset 45601 d5178f19b671
parent 45600 1bbbac9a0cb0
child 46215 0da9433f959e
equal deleted inserted replaced
45600:1bbbac9a0cb0 45601:d5178f19b671
   296         bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
   296         bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
   297     val (_, ctxt') = lthy |> prep_vars raw_fixes |-> Proof_Context.add_fixes;
   297     val (_, ctxt') = lthy |> prep_vars raw_fixes |-> Proof_Context.add_fixes;
   298 
   298 
   299     val facts' = facts
   299     val facts' = facts
   300       |> Attrib.partial_evaluation ctxt'
   300       |> Attrib.partial_evaluation ctxt'
   301       |> Element.facts_map (Element.transform_ctxt (Proof_Context.export_morphism ctxt' lthy));
   301       |> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
   302     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
   302     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
   303     val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
   303     val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
   304   in (res, lthy') end;
   304   in (res, lthy') end;
   305 
   305 
   306 in
   306 in