avoid odd reinit after sublocale declaration
authorhaftmann
Wed Apr 24 11:32:54 2013 +0200 (2013-04-24)
changeset 51750cb154917a496
parent 51749 c27bb7994bd3
child 51752 c45ca48b526e
avoid odd reinit after sublocale declaration
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Apr 24 10:23:47 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Apr 24 11:32:54 2013 +0200
     1.3 @@ -829,7 +829,7 @@
     1.4  
     1.5  fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
     1.6  
     1.7 -fun note_eqns_register note activate reinit deps witss eqns attrss export export' ctxt =
     1.8 +fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
     1.9    let
    1.10      val facts = 
    1.11        (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    1.12 @@ -843,22 +843,23 @@
    1.13    in
    1.14      ctxt'
    1.15      |> fold activate' dep_morphs
    1.16 -    |> reinit
    1.17    end;
    1.18  
    1.19  fun generic_interpretation prep_expr parse_prop prep_attr setup_proof note add_registration
    1.20 -    reinit expression raw_eqns initial_ctxt = 
    1.21 +    expression raw_eqns initial_ctxt = 
    1.22    let
    1.23      val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) = 
    1.24        read_interpretation prep_expr parse_prop prep_attr expression raw_eqns initial_ctxt;
    1.25      fun after_qed witss eqns =
    1.26 -      note_eqns_register note add_registration reinit deps witss eqns attrss export export';
    1.27 +      note_eqns_register note add_registration deps witss eqns attrss export export';
    1.28    in setup_proof after_qed propss eqns goal_ctxt end;
    1.29  
    1.30  val activate_proof = Context.proof_map ooo Locale.add_registration;
    1.31  val activate_local_theory = Local_Theory.target ooo activate_proof;
    1.32  val add_registration = Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
    1.33 -fun add_dependency locale = Local_Theory.raw_theory ooo Locale.add_dependency locale;
    1.34 +fun add_dependency locale dep_morph mixin export =
    1.35 +  (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
    1.36 +  #> activate_local_theory dep_morph mixin export;
    1.37  fun add_dependency_global locale = Proof_Context.background_theory ooo Locale.add_dependency locale;
    1.38  
    1.39  fun gen_interpret prep_expr parse_prop prep_attr expression raw_eqns int state =
    1.40 @@ -870,7 +871,7 @@
    1.41        Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" propss eqns goal_ctxt int state;
    1.42    in
    1.43      generic_interpretation prep_expr parse_prop prep_attr setup_proof
    1.44 -      Attrib.local_notes activate_proof I expression raw_eqns ctxt
    1.45 +      Attrib.local_notes activate_proof expression raw_eqns ctxt
    1.46    end;
    1.47  
    1.48  fun gen_interpretation prep_expr parse_prop prep_attr expression raw_eqns lthy =
    1.49 @@ -881,7 +882,7 @@
    1.50    in
    1.51      lthy
    1.52      |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
    1.53 -        Local_Theory.notes_kind activate I expression raw_eqns
    1.54 +        Local_Theory.notes_kind activate expression raw_eqns
    1.55    end;
    1.56  
    1.57  fun gen_sublocale prep_expr parse_prop prep_attr expression raw_eqns lthy =
    1.58 @@ -893,7 +894,7 @@
    1.59    in
    1.60      lthy
    1.61      |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
    1.62 -        Local_Theory.notes_kind (add_dependency locale) (Named_Target.reinit lthy) expression raw_eqns
    1.63 +        Local_Theory.notes_kind (add_dependency locale) expression raw_eqns
    1.64    end;
    1.65    
    1.66  fun gen_sublocale_global prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression raw_eqns thy =
    1.67 @@ -903,7 +904,7 @@
    1.68      thy
    1.69      |> Named_Target.init before_exit locale
    1.70      |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
    1.71 -        Local_Theory.notes_kind (add_dependency_global locale) I expression raw_eqns
    1.72 +        Local_Theory.notes_kind (add_dependency_global locale) expression raw_eqns
    1.73    end;
    1.74  
    1.75  in
    1.76 @@ -916,11 +917,10 @@
    1.77          | NONE => error "Not in a named target";
    1.78      val is_theory = (target = "");
    1.79      val activate = if is_theory then add_registration else add_dependency target;
    1.80 -    val reinit = if is_theory then I else Named_Target.reinit lthy;
    1.81    in
    1.82      lthy
    1.83      |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
    1.84 -        Local_Theory.notes_kind activate reinit expression raw_eqns
    1.85 +        Local_Theory.notes_kind activate expression raw_eqns
    1.86    end;
    1.87  
    1.88  fun ephemeral_interpretation expression raw_eqns lthy =
    1.89 @@ -932,7 +932,7 @@
    1.90      lthy
    1.91      |> Local_Theory.mark_brittle
    1.92      |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
    1.93 -        Local_Theory.notes_kind activate_local_theory I expression raw_eqns
    1.94 +        Local_Theory.notes_kind activate_local_theory expression raw_eqns
    1.95    end;
    1.96  
    1.97  fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;