src/Pure/Isar/expression.ML
changeset 30764 3e3e7aa0cc7a
parent 30763 6976521b4263
child 30774 5daee9354a9c
child 30783 275577cefaa8
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 28 17:53:33 2009 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Mar 28 20:25:23 2009 +0100
     1.3 @@ -352,7 +352,7 @@
     1.4          val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
     1.5          val inst''' = insts'' |> List.last |> snd |> snd;
     1.6          val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
     1.7 -        val ctxt'' = Locale.activate_declarations thy (loc, morph) ctxt;
     1.8 +        val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
     1.9        in (i + 1, insts', ctxt'') end;
    1.10  
    1.11      fun prep_elem insts raw_elem (elems, ctxt) =
    1.12 @@ -437,7 +437,7 @@
    1.13      (* Declare parameters and imported facts *)
    1.14      val context' = context |>
    1.15        fix_params fixed |>
    1.16 -      fold Locale.activate_local_facts deps;
    1.17 +      fold (Context.proof_map o Locale.activate_facts) deps;
    1.18      val (elems', _) = context' |>
    1.19        ProofContext.set_stmt true |>
    1.20        activate elems;
    1.21 @@ -787,7 +787,7 @@
    1.22      fun after_qed witss = ProofContext.theory
    1.23        (fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
    1.24          (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
    1.25 -      (fn thy => fold_rev Locale.activate_global_facts
    1.26 +      (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
    1.27          (Locale.get_registrations thy) thy));
    1.28    in Element.witness_proof after_qed propss goal_ctxt end;
    1.29  
    1.30 @@ -827,7 +827,7 @@
    1.31      fun store_eqns_activate regs [] thy =
    1.32            thy
    1.33            |> fold (fn (name, morph) =>
    1.34 -               Locale.activate_global_facts (name, morph $> export)) regs
    1.35 +               Context.theory_map (Locale.activate_facts (name, morph $> export))) regs
    1.36        | store_eqns_activate regs eqs thy =
    1.37            let
    1.38              val eqs' = eqs |> map (Morphism.thm (export' $> export) #>
    1.39 @@ -839,7 +839,7 @@
    1.40              thy
    1.41              |> fold (fn (name, morph) =>
    1.42                  Locale.amend_registration eq_morph (name, morph) #>
    1.43 -                Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs
    1.44 +                Context.theory_map (Locale.activate_facts (name, morph $> eq_morph $> export))) regs
    1.45              |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs')
    1.46              |> snd
    1.47            end;
    1.48 @@ -873,7 +873,7 @@
    1.49      fun store_reg (name, morph) thms =
    1.50        let
    1.51          val morph' = morph $> Element.satisfy_morphism thms $> export;
    1.52 -      in Locale.activate_local_facts (name, morph') end;
    1.53 +      in Context.proof_map (Locale.activate_facts (name, morph')) end;
    1.54  
    1.55      fun after_qed wits =
    1.56        Proof.map_context (fold2 store_reg regs wits);