src/Pure/Isar/expression.ML
changeset 47249 c0481c3c2a6c
parent 47068 2027ff3136cc
child 47287 8f06d8ac4609
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Apr 01 19:04:52 2012 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Apr 01 19:07:32 2012 +0200
     1.3 @@ -816,7 +816,7 @@
     1.4  local
     1.5  
     1.6  fun note_eqns_register deps witss attrss eqns export export' =
     1.7 -  Element.generic_note_thmss Thm.lemmaK
     1.8 +  Attrib.generic_notes Thm.lemmaK
     1.9      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
    1.10    #-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
    1.11    #-> (fn eqns => fold (fn ((dep, morph), wits) =>
    1.12 @@ -885,12 +885,10 @@
    1.13  
    1.14  fun note_eqns_dependency target deps witss attrss eqns export export' ctxt =
    1.15    let
    1.16 -    val thy = Proof_Context.theory_of ctxt;
    1.17 -
    1.18      val facts =
    1.19        (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    1.20      val eqns' = ctxt
    1.21 -      |> Proof_Context.note_thmss Thm.lemmaK (Attrib.map_facts (map (Attrib.attribute_i thy)) facts)
    1.22 +      |> Attrib.local_notes Thm.lemmaK facts
    1.23        |-> (fn facts => `(fn ctxt => meta_rewrite ctxt (maps snd facts)))
    1.24        |> fst;  (* FIXME duplication to add_thmss *)
    1.25    in