src/Pure/Isar/expression.ML
changeset 31988 801aabf9f376
parent 30786 461f7b5f16a2
child 31989 a290c36e94d6
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Jul 10 07:59:28 2009 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Jul 10 07:59:29 2009 +0200
     1.3 @@ -796,14 +796,9 @@
     1.4    let
     1.5      val target = intern thy raw_target;
     1.6      val target_ctxt = Locale.init target thy;
     1.7 -
     1.8      val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
     1.9 -
    1.10      fun after_qed witss = ProofContext.theory
    1.11 -      (fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
    1.12 -        (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
    1.13 -      (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
    1.14 -        (Locale.get_registrations thy) thy));
    1.15 +      (Locale.add_dependencies target (deps ~~ witss) export);
    1.16    in Element.witness_proof after_qed propss goal_ctxt end;
    1.17  
    1.18  in
    1.19 @@ -860,7 +855,7 @@
    1.20            end;
    1.21  
    1.22      fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits)
    1.23 -        #-> (fn regs => store_eqns_activate regs eqs));
    1.24 +      #-> (fn regs => store_eqns_activate regs eqs));
    1.25  
    1.26    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    1.27