src/Pure/Isar/locale.ML
changeset 30775 71f777103225
parent 30773 6cc9964436c3
child 30777 9960ff945c52
     1.1 --- a/src/Pure/Isar/locale.ML	Sun Mar 29 16:13:44 2009 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Sun Mar 29 17:47:50 2009 +0200
     1.3 @@ -293,52 +293,20 @@
     1.4  
     1.5  (** Public activation functions **)
     1.6  
     1.7 -local
     1.8 -
     1.9 -fun init_elem (Fixes fixes) (Context.Proof ctxt) =
    1.10 -      Context.Proof (ProofContext.add_fixes fixes ctxt |> snd)
    1.11 -  | init_elem (Assumes assms) (Context.Proof ctxt) =
    1.12 -      let
    1.13 -        val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms;
    1.14 -        val ctxt' = ctxt
    1.15 -          |> fold Variable.auto_fixes (maps (map fst o snd) assms')
    1.16 -          |> ProofContext.add_assms_i Assumption.assume_export assms' |> snd;
    1.17 -      in Context.Proof ctxt' end
    1.18 -  | init_elem (Defines defs) (Context.Proof ctxt) =
    1.19 -      let
    1.20 -        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
    1.21 -        val ctxt' = ctxt
    1.22 -          |> fold Variable.auto_fixes (map (fst o snd) defs')
    1.23 -          |> ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs')
    1.24 -          |> snd;
    1.25 -      in Context.Proof ctxt' end
    1.26 -  | init_elem (Notes (kind, facts)) (Context.Proof ctxt) =
    1.27 -      let
    1.28 -        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
    1.29 -      in Context.Proof (ProofContext.note_thmss kind facts' ctxt |> snd) end
    1.30 -  | init_elem (Notes (kind, facts)) (Context.Theory thy) =
    1.31 -      let
    1.32 -        val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
    1.33 -      in Context.Theory (PureThy.note_thmss kind facts' thy |> snd) end
    1.34 -  | init_elem _ (Context.Theory _) = raise Fail "Bad context element in global theory";
    1.35 -
    1.36 -in
    1.37 -
    1.38 -fun activate_declarations dep ctxt =
    1.39 +fun activate_declarations dep = Context.proof_map (fn context =>
    1.40    let
    1.41 -    val context = Context.Proof ctxt;
    1.42      val thy = Context.theory_of context;
    1.43      val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents;
    1.44 -  in Context.the_proof context' end;
    1.45 +  in context' end);
    1.46  
    1.47  fun activate_facts dep context =
    1.48    let
    1.49      val thy = Context.theory_of context;
    1.50 -    val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of) thy;
    1.51 +    val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy;
    1.52    in roundup thy activate dep (get_idents context, context) |-> put_idents end;
    1.53  
    1.54  fun init name thy =
    1.55 -  activate_all name thy init_elem (Element.transfer_morphism o Context.theory_of)
    1.56 +  activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
    1.57      ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
    1.58  
    1.59  fun print_locale thy show_facts raw_name =
    1.60 @@ -355,8 +323,6 @@
    1.61      |> Pretty.writeln
    1.62    end;
    1.63  
    1.64 -end;
    1.65 -
    1.66  
    1.67  (*** Registrations: interpretations in theories ***)
    1.68  
    1.69 @@ -398,7 +364,6 @@
    1.70    end;
    1.71  
    1.72  
    1.73 -
    1.74  (*** Storing results ***)
    1.75  
    1.76  (* Theorems *)