src/Pure/Isar/expression.ML
changeset 45290 f599ac41e7f5
parent 45289 25e9e7f527b4
child 45587 2f2251ec4279
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Oct 28 15:38:41 2011 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Oct 28 17:15:52 2011 +0200
     1.3 @@ -771,10 +771,10 @@
     1.4  
     1.5      val notes' = body_elems |>
     1.6        map (defines_to_notes thy') |>
     1.7 -      map (Element.morph_ctxt a_satisfy) |>
     1.8 +      map (Element.transform_ctxt a_satisfy) |>
     1.9        (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
    1.10        fst |>
    1.11 -      map (Element.morph_ctxt b_satisfy) |>
    1.12 +      map (Element.transform_ctxt b_satisfy) |>
    1.13        map_filter (fn Notes notes => SOME notes | _ => NONE);
    1.14  
    1.15      val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
    1.16 @@ -823,7 +823,7 @@
    1.17      |-> (fn eqns => fold (fn ((dep, morph), wits) =>
    1.18        fn context =>
    1.19          Locale.add_registration (dep, morph $> Element.satisfy_morphism
    1.20 -            (map (Element.morph_witness export') wits))
    1.21 +            (map (Element.transform_witness export') wits))
    1.22            (Element.eq_morphism (Context.theory_of context) eqns |>
    1.23              Option.map (rpair true))
    1.24            export context) (deps ~~ witss))
    1.25 @@ -902,7 +902,7 @@
    1.26        fn theory =>
    1.27          Locale.add_dependency target
    1.28            (dep, morph $> Element.satisfy_morphism
    1.29 -            (map (Element.morph_witness export') wits))
    1.30 +            (map (Element.transform_witness export') wits))
    1.31            (Element.eq_morphism theory eqns' |> Option.map (rpair true))
    1.32            export theory) (deps ~~ witss))
    1.33    end;