more structural integrity;
authorwenzelm
Mon Jun 03 23:58:20 2019 +0200 (13 months ago)
changeset 703139c19e15c8548
parent 70312 56f96489478c
child 70314 6d6839a948cf
more structural integrity;
src/Pure/assumption.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/assumption.ML	Mon Jun 03 23:29:05 2019 +0200
     1.2 +++ b/src/Pure/assumption.ML	Mon Jun 03 23:58:20 2019 +0200
     1.3 @@ -108,10 +108,14 @@
     1.4  
     1.5  (* export *)
     1.6  
     1.7 +fun normalize ctxt0 th0 =
     1.8 +  let val (ctxt, th) = Thm.join_transfer_context (ctxt0, th0)
     1.9 +  in Raw_Simplifier.norm_hhf_protect ctxt th end;
    1.10 +
    1.11  fun export is_goal inner outer =
    1.12 -  Raw_Simplifier.norm_hhf_protect inner #>
    1.13 +  normalize inner #>
    1.14    fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
    1.15 -  Raw_Simplifier.norm_hhf_protect outer;
    1.16 +  normalize outer;
    1.17  
    1.18  fun export_term inner outer =
    1.19    fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
    1.20 @@ -122,6 +126,8 @@
    1.21      val term = export_term inner outer;
    1.22      val typ = Logic.type_map term;
    1.23    in
    1.24 +    Morphism.transfer_morphism' inner $>
    1.25 +    Morphism.transfer_morphism' outer $>
    1.26      Morphism.morphism "Assumption.export"
    1.27        {binding = [], typ = [typ], term = [term], fact = [map thm]}
    1.28    end;
     2.1 --- a/src/Pure/thm.ML	Mon Jun 03 23:29:05 2019 +0200
     2.2 +++ b/src/Pure/thm.ML	Mon Jun 03 23:58:20 2019 +0200
     2.3 @@ -90,6 +90,7 @@
     2.4    val transfer': Proof.context -> thm -> thm
     2.5    val transfer'': Context.generic -> thm -> thm
     2.6    val join_transfer: theory -> thm -> thm
     2.7 +  val join_transfer_context: Proof.context * thm -> Proof.context * thm
     2.8    val renamed_prop: term -> thm -> thm
     2.9    val weaken: cterm -> thm -> thm
    2.10    val weaken_sorts: sort list -> cterm -> cterm
    2.11 @@ -535,6 +536,11 @@
    2.12    if Context.subthy_id (Context.theory_id thy, theory_id th) then th
    2.13    else transfer thy th;
    2.14  
    2.15 +fun join_transfer_context (ctxt, th) =
    2.16 +  if Context.subthy_id (Context.theory_id (Proof_Context.theory_of ctxt), theory_id th) then
    2.17 +    (Context.raw_transfer (theory_of_thm th) ctxt, th)
    2.18 +  else (ctxt, transfer' ctxt th);
    2.19 +
    2.20  
    2.21  (* matching *)
    2.22