src/Pure/Isar/expression.ML
changeset 51727 cf97bb5bbc90
parent 51565 5e9fdbdf88ce
child 51728 0f6e8c4144a5
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
     1.3 @@ -819,22 +819,28 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun note_eqns_register deps witss attrss eqns export export' =
     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 -    fn context =>
    1.13 +fun note_eqns_register deps witss attrss eqns export export' context =
    1.14 +  let
    1.15 +    val facts = 
    1.16 +      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    1.17 +    val (eqns', context') = context 
    1.18 +      |> Attrib.generic_notes Thm.lemmaK facts
    1.19 +      |-> (fn facts' => `(fn context'' => meta_rewrite (Context.proof_of context'') (maps snd facts')));
    1.20 +  in
    1.21 +    context'
    1.22 +    |> fold2 (fn (dep, morph) => fn wits => fn context'' =>
    1.23        Locale.add_registration
    1.24          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
    1.25 -        (Element.eq_morphism (Context.theory_of context) eqns |> Option.map (rpair true))
    1.26 -        export context) (deps ~~ witss));
    1.27 +        (Element.eq_morphism (Context.theory_of context'') eqns' |> Option.map (rpair true))
    1.28 +        export context'') deps witss
    1.29 +  end;
    1.30  
    1.31  fun gen_interpretation prep_expr parse_prop prep_attr
    1.32      expression equations thy =
    1.33    let
    1.34 -    val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global thy
    1.35 -      |> prep_expr expression;
    1.36 +    val initial_ctxt = Proof_Context.init_global thy;
    1.37 +
    1.38 +    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    1.39      val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.40  
    1.41      val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
    1.42 @@ -891,27 +897,27 @@
    1.43    let
    1.44      val facts =
    1.45        (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    1.46 -    val eqns' = ctxt
    1.47 +    val (eqns', _) = ctxt (* FIXME duplication to add_thmss *)
    1.48        |> Attrib.local_notes Thm.lemmaK facts
    1.49 -      |-> (fn facts => `(fn ctxt => meta_rewrite ctxt (maps snd facts)))
    1.50 -      |> fst;  (* FIXME duplication to add_thmss *)
    1.51 +      |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts')));
    1.52    in
    1.53      ctxt
    1.54      |> Locale.add_thmss target Thm.lemmaK (Attrib.partial_evaluation ctxt facts)
    1.55 -    |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
    1.56 +    |> Proof_Context.background_theory (fold2 (fn (dep, morph) => fn wits =>
    1.57        fn thy =>
    1.58          Locale.add_dependency target
    1.59            (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
    1.60            (Element.eq_morphism thy eqns' |> Option.map (rpair true))
    1.61 -          export thy) (deps ~~ witss))
    1.62 +          export thy) deps witss)
    1.63    end;
    1.64  
    1.65  fun gen_sublocale prep_expr prep_loc parse_prop prep_attr
    1.66      before_exit raw_target expression equations thy =
    1.67    let
    1.68      val target = prep_loc thy raw_target;
    1.69 -    val target_ctxt = Named_Target.init before_exit target thy;
    1.70 -    val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
    1.71 +    val initial_ctxt = Named_Target.init before_exit target thy;
    1.72 +
    1.73 +    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    1.74      val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.75  
    1.76      val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;