tuned
authorhaftmann
Mon Jan 19 08:16:43 2009 +0100 (2009-01-19)
changeset 29559fe9cfe076c23
parent 29558 9846af6c6d6a
child 29560 fa6c5d62adf5
child 29561 d8c2712749b8
tuned
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Mon Jan 19 08:16:42 2009 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Mon Jan 19 08:16:43 2009 +0100
     1.3 @@ -806,15 +806,15 @@
     1.4  
     1.5      val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
     1.6      
     1.7 -    fun store_dep ((name, morph), thms) =
     1.8 +    fun store_dep (name, morph) thms =
     1.9        Locale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export);
    1.10  
    1.11      fun after_qed results =
    1.12        ProofContext.theory (
    1.13          (* store dependencies *)
    1.14 -        fold store_dep (deps ~~ prep_result propss results) #>
    1.15 +        fold2 store_dep deps (prep_result propss results) #>
    1.16          (* propagate registrations *)
    1.17 -        (fn thy => fold_rev (fn reg => Locale.activate_global_facts reg)
    1.18 +        (fn thy => fold_rev Locale.activate_global_facts
    1.19            (Locale.get_registrations thy) thy));
    1.20    in
    1.21      goal_ctxt |>