src/Pure/Isar/expression.ML
changeset 46858 05f30c796f95
parent 46856 28909eecdf5b
child 46899 58110c1e02bc
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 10 19:49:32 2012 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Mar 10 20:02:15 2012 +0100
     1.3 @@ -814,17 +814,15 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun note_eqns_register deps witss attrss eqns export export' context =
     1.8 -  context
     1.9 -  |> Element.generic_note_thmss Thm.lemmaK
    1.10 +fun note_eqns_register deps witss attrss eqns export export' =
    1.11 +  Element.generic_note_thmss Thm.lemmaK
    1.12      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
    1.13 -  |-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
    1.14 -  |-> (fn eqns => fold (fn ((dep, morph), wits) =>
    1.15 +  #-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
    1.16 +  #-> (fn eqns => fold (fn ((dep, morph), wits) =>
    1.17      fn context =>
    1.18 -      Locale.add_registration (dep, morph $> Element.satisfy_morphism
    1.19 -          (map (Element.transform_witness export') wits))
    1.20 -        (Element.eq_morphism (Context.theory_of context) eqns |>
    1.21 -          Option.map (rpair true))
    1.22 +      Locale.add_registration
    1.23 +        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
    1.24 +        (Element.eq_morphism (Context.theory_of context) eqns |> Option.map (rpair true))
    1.25          export context) (deps ~~ witss));
    1.26  
    1.27  fun gen_interpretation prep_expr parse_prop prep_attr