src/Pure/Isar/expression.ML
changeset 54879 a9397557da56
parent 54878 710e8f36a917
child 54883 dd04a8b654fc
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Dec 29 23:21:14 2013 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Mon Dec 30 12:43:06 2013 +0100
     1.3 @@ -413,7 +413,7 @@
     1.4      val deps = map (finish_inst ctxt6) insts;
     1.5      val elems'' = map (finish_elem (ctxt1, ctxt6) parms do_close) elems';
     1.6  
     1.7 -  in ((fixed, deps, elems'', concl), (parms, ctxt7)) end
     1.8 +  in ((fixed, deps, elems'', concl), (parms, ctxt7)) end;
     1.9  
    1.10  in
    1.11  
    1.12 @@ -836,13 +836,17 @@
    1.13      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.14    in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
    1.15  
    1.16 -val cert_interpretation = prep_interpretation cert_goal_expression (K I) (K I);
    1.17 -val read_interpretation = prep_interpretation read_goal_expression Syntax.parse_prop Attrib.intern_src;
    1.18 +val cert_interpretation =
    1.19 +  prep_interpretation cert_goal_expression (K I) (K I);
    1.20 +
    1.21 +val read_interpretation =
    1.22 +  prep_interpretation read_goal_expression Syntax.parse_prop Attrib.intern_src;
    1.23  
    1.24  
    1.25  (* generic interpretation machinery *)
    1.26  
    1.27 -fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
    1.28 +fun meta_rewrite eqns ctxt =
    1.29 +  (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
    1.30  
    1.31  fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
    1.32    let
    1.33 @@ -851,19 +855,23 @@
    1.34      val (eqns', ctxt') = ctxt
    1.35        |> note Thm.lemmaK facts
    1.36        |-> meta_rewrite;
    1.37 -    val dep_morphs = map2 (fn (dep, morph) => fn wits =>
    1.38 -      (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
    1.39 -    fun activate' dep_morph ctxt = activate dep_morph
    1.40 -      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
    1.41 +    val dep_morphs =
    1.42 +      map2 (fn (dep, morph) => fn wits =>
    1.43 +          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)))
    1.44 +        deps witss;
    1.45 +    fun activate' dep_morph ctxt =
    1.46 +      activate dep_morph
    1.47 +        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns'))
    1.48 +        export ctxt;
    1.49    in
    1.50      ctxt'
    1.51      |> fold activate' dep_morphs
    1.52    end;
    1.53  
    1.54  fun generic_interpretation prep_interpretation setup_proof note activate
    1.55 -    expression raw_eqns initial_ctxt = 
    1.56 +    expression raw_eqns initial_ctxt =
    1.57    let
    1.58 -    val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) = 
    1.59 +    val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) =
    1.60        prep_interpretation expression raw_eqns initial_ctxt;
    1.61      fun after_qed witss eqns =
    1.62        note_eqns_register note activate deps witss eqns attrss export export';
    1.63 @@ -876,9 +884,11 @@
    1.64    let
    1.65      val _ = Proof.assert_forward_or_chain state;
    1.66      val ctxt = Proof.context_of state;
    1.67 -    fun lift_after_qed after_qed witss eqns = Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
    1.68 -    fun setup_proof after_qed propss eqns goal_ctxt = 
    1.69 -      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" propss eqns goal_ctxt int state;
    1.70 +    fun lift_after_qed after_qed witss eqns =
    1.71 +      Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
    1.72 +    fun setup_proof after_qed propss eqns goal_ctxt =
    1.73 +      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
    1.74 +        propss eqns goal_ctxt int state;
    1.75    in
    1.76      generic_interpretation prep_interpretation setup_proof
    1.77        Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
    1.78 @@ -910,7 +920,8 @@
    1.79  
    1.80  (* special case: global sublocale command *)
    1.81  
    1.82 -fun gen_sublocale_global prep_loc prep_interpretation before_exit raw_locale expression raw_eqns thy =
    1.83 +fun gen_sublocale_global prep_loc prep_interpretation
    1.84 +    before_exit raw_locale expression raw_eqns thy =
    1.85    thy
    1.86    |> Named_Target.init before_exit (prep_loc thy raw_locale)
    1.87    |> gen_local_theory_interpretation prep_interpretation subscribe_locale_only expression raw_eqns
    1.88 @@ -923,15 +934,21 @@
    1.89  fun interpret x = gen_interpret cert_interpretation x;
    1.90  fun interpret_cmd x = gen_interpret read_interpretation x;
    1.91  
    1.92 -fun permanent_interpretation x = gen_local_theory_interpretation cert_interpretation subscribe x;
    1.93 +fun permanent_interpretation x =
    1.94 +  gen_local_theory_interpretation cert_interpretation subscribe x;
    1.95  
    1.96 -fun ephemeral_interpretation x = gen_local_theory_interpretation cert_interpretation (K Local_Theory.activate) x;
    1.97 +fun ephemeral_interpretation x =
    1.98 +  gen_local_theory_interpretation cert_interpretation (K Local_Theory.activate) x;
    1.99  
   1.100 -fun interpretation x = gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
   1.101 -fun interpretation_cmd x = gen_local_theory_interpretation read_interpretation subscribe_or_activate x;
   1.102 +fun interpretation x =
   1.103 +  gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
   1.104 +fun interpretation_cmd x =
   1.105 +  gen_local_theory_interpretation read_interpretation subscribe_or_activate x;
   1.106  
   1.107 -fun sublocale x = gen_local_theory_interpretation cert_interpretation subscribe_locale_only x;
   1.108 -fun sublocale_cmd x = gen_local_theory_interpretation read_interpretation subscribe_locale_only x;
   1.109 +fun sublocale x =
   1.110 +  gen_local_theory_interpretation cert_interpretation subscribe_locale_only x;
   1.111 +fun sublocale_cmd x =
   1.112 +  gen_local_theory_interpretation read_interpretation subscribe_locale_only x;
   1.113  
   1.114  fun sublocale_global x = gen_sublocale_global (K I) cert_interpretation x;
   1.115  fun sublocale_global_cmd x = gen_sublocale_global Locale.check read_interpretation x;