misc tuning;
authorwenzelm
Sat Nov 19 15:34:37 2011 +0100 (2011-11-19)
changeset 455885eb47a1e4ca7
parent 45587 2f2251ec4279
child 45589 bb944d58ac19
misc tuning;
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Nov 19 15:04:36 2011 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Nov 19 15:34:37 2011 +0100
     1.3 @@ -807,37 +807,34 @@
     1.4        |> Variable.export_terms deps_ctxt ctxt
     1.5    end;
     1.6  
     1.7 +fun meta_rewrite ctxt = map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def);
     1.8 +
     1.9 +
    1.10  (** Interpretation in theories and proof contexts **)
    1.11  
    1.12  local
    1.13  
    1.14  fun note_eqns_register deps witss attrss eqns export export' context =
    1.15 -  let
    1.16 -    fun meta_rewrite context =
    1.17 -      map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
    1.18 -        maps snd;
    1.19 -  in
    1.20 -    context
    1.21 -    |> Element.generic_note_thmss Thm.lemmaK
    1.22 -      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
    1.23 -    |-> (fn facts => `(fn context => meta_rewrite context facts))
    1.24 -    |-> (fn eqns => fold (fn ((dep, morph), wits) =>
    1.25 -      fn context =>
    1.26 -        Locale.add_registration (dep, morph $> Element.satisfy_morphism
    1.27 -            (map (Element.transform_witness export') wits))
    1.28 -          (Element.eq_morphism (Context.theory_of context) eqns |>
    1.29 -            Option.map (rpair true))
    1.30 -          export context) (deps ~~ witss))
    1.31 -  end;
    1.32 +  context
    1.33 +  |> Element.generic_note_thmss Thm.lemmaK
    1.34 +    (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
    1.35 +  |-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
    1.36 +  |-> (fn eqns => fold (fn ((dep, morph), wits) =>
    1.37 +    fn context =>
    1.38 +      Locale.add_registration (dep, morph $> Element.satisfy_morphism
    1.39 +          (map (Element.transform_witness export') wits))
    1.40 +        (Element.eq_morphism (Context.theory_of context) eqns |>
    1.41 +          Option.map (rpair true))
    1.42 +        export context) (deps ~~ witss));
    1.43  
    1.44  fun gen_interpretation prep_expr parse_prop prep_attr
    1.45 -    expression equations theory =
    1.46 +    expression equations thy =
    1.47    let
    1.48 -    val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global theory
    1.49 +    val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global thy
    1.50        |> prep_expr expression;
    1.51      val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.52  
    1.53 -    val attrss = map (apsnd (map (prep_attr theory)) o fst) equations;
    1.54 +    val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
    1.55      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.56      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.57  
    1.58 @@ -852,17 +849,18 @@
    1.59    let
    1.60      val _ = Proof.assert_forward_or_chain state;
    1.61      val ctxt = Proof.context_of state;
    1.62 -    val theory = Proof_Context.theory_of ctxt;
    1.63 +    val thy = Proof_Context.theory_of ctxt;
    1.64  
    1.65      val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
    1.66      val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.67  
    1.68 -    val attrss = map (apsnd (map (prep_attr theory)) o fst) equations;
    1.69 +    val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
    1.70      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.71      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.72  
    1.73 -    fun after_qed witss eqns = (Proof.map_context o Context.proof_map)
    1.74 -      (note_eqns_register deps witss attrss eqns export export');
    1.75 +    fun after_qed witss eqns =
    1.76 +      (Proof.map_context o Context.proof_map)
    1.77 +        (note_eqns_register deps witss attrss eqns export export');
    1.78    in
    1.79      state
    1.80      |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int
    1.81 @@ -887,25 +885,24 @@
    1.82  
    1.83  fun note_eqns_dependency target deps witss attrss eqns export export' ctxt =
    1.84    let
    1.85 -    fun meta_rewrite ctxt =
    1.86 -      map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) o maps snd;
    1.87 +    val thy = Proof_Context.theory_of ctxt;
    1.88 +
    1.89      val facts =
    1.90        (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    1.91 -    val eqns' = ctxt |> Context.Proof
    1.92 -      |> Element.generic_note_thmss Thm.lemmaK facts
    1.93 -      |> apsnd Context.the_proof  (* FIXME Context.proof_map_result *)
    1.94 -      |-> (fn facts => `(fn ctxt => meta_rewrite ctxt facts))
    1.95 +    val eqns' = ctxt
    1.96 +      |> Proof_Context.note_thmss Thm.lemmaK (Attrib.map_facts (map (Attrib.attribute_i thy)) facts)
    1.97 +      |-> (fn facts => `(fn ctxt => meta_rewrite ctxt (maps snd facts)))
    1.98        |> fst;  (* FIXME duplication to add_thmss *)
    1.99    in
   1.100      ctxt
   1.101      |> Locale.add_thmss target Thm.lemmaK facts
   1.102      |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
   1.103 -      fn theory =>
   1.104 +      fn thy =>
   1.105          Locale.add_dependency target
   1.106            (dep, morph $> Element.satisfy_morphism
   1.107              (map (Element.transform_witness export') wits))
   1.108 -          (Element.eq_morphism theory eqns' |> Option.map (rpair true))
   1.109 -          export theory) (deps ~~ witss))
   1.110 +          (Element.eq_morphism thy eqns' |> Option.map (rpair true))
   1.111 +          export thy) (deps ~~ witss))
   1.112    end;
   1.113  
   1.114  fun gen_sublocale prep_expr intern parse_prop prep_attr