1.1 --- a/src/Pure/Isar/element.ML	Sun Mar 29 16:13:44 2009 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Sun Mar 29 17:47:50 2009 +0200
     1.3 @@ -60,6 +60,7 @@
     1.4      (Attrib.binding * (thm list * Attrib.src list) list) list
     1.5    val eq_morphism: theory -> thm list -> morphism
     1.6    val transfer_morphism: theory -> morphism
     1.7 +  val init: context_i -> Context.generic -> Context.generic
     1.8    val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context
     1.9    val activate_i: context_i list -> Proof.context -> context_i list * Proof.context
    1.10  end;
    1.11 @@ -481,62 +482,62 @@
    1.12  
    1.13  
    1.14  
    1.15 -(** activate in context, return elements and facts **)
    1.16 +(** activate in context **)
    1.17  
    1.18 -local
    1.19 +(* init *)
    1.20  
    1.21 -fun activate_elem (Fixes fixes) ctxt =
    1.22 -      ctxt |> ProofContext.add_fixes fixes |> snd
    1.23 -  | activate_elem (Constrains _) ctxt =
    1.24 -      ctxt
    1.25 -  | activate_elem (Assumes asms) ctxt =
    1.26 +fun init (Fixes fixes) = Context.map_proof (ProofContext.add_fixes fixes #> #2)
    1.27 +  | init (Constrains _) = I
    1.28 +  | init (Assumes asms) = Context.map_proof (fn ctxt =>
    1.29        let
    1.30          val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
    1.31 -        val ts = maps (map #1 o #2) asms';
    1.32 -        val (_, ctxt') =
    1.33 -          ctxt |> fold Variable.auto_fixes ts
    1.34 -          |> ProofContext.add_assms_i Assumption.presume_export asms';
    1.35 -      in ctxt' end
    1.36 -  | activate_elem (Defines defs) ctxt =
    1.37 +        val (_, ctxt') = ctxt
    1.38 +          |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
    1.39 +          |> ProofContext.add_assms_i Assumption.assume_export asms';
    1.40 +      in ctxt' end)
    1.41 +  | init (Defines defs) = Context.map_proof (fn ctxt =>
    1.42        let
    1.43          val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
    1.44          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
    1.45 -            let val ((c, _), t') = LocalDefs.cert_def ctxt t
    1.46 +            let val ((c, _), t') = LocalDefs.cert_def ctxt t  (* FIXME adapt ps? *)
    1.47              in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
    1.48 -        val (_, ctxt') =
    1.49 -          ctxt |> fold (Variable.auto_fixes o #1) asms
    1.50 +        val (_, ctxt') = ctxt
    1.51 +          |> fold Variable.auto_fixes (map #1 asms)
    1.52            |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
    1.53 -      in ctxt' end
    1.54 -  | activate_elem (Notes (kind, facts)) ctxt =
    1.55 +      in ctxt' end)
    1.56 +  | init (Notes (kind, facts)) = (fn context =>
    1.57        let
    1.58 -        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
    1.59 -        val (res, ctxt') = ctxt |> ProofContext.note_thmss kind facts';
    1.60 -      in ctxt' end;
    1.61 +        val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
    1.62 +        val context' = context |> Context.mapping
    1.63 +          (PureThy.note_thmss kind facts' #> #2)
    1.64 +          (ProofContext.note_thmss kind facts' #> #2);
    1.65 +      in context' end);
    1.66 +
    1.67 +
    1.68 +(* activate *)
    1.69 +
    1.70 +local
    1.71  
    1.72  fun gen_activate prep_facts raw_elems ctxt =
    1.73    let
    1.74 -    fun activate elem ctxt =
    1.75 -      let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem
    1.76 -      in (elem', activate_elem elem' ctxt) end
    1.77 +    fun activate elem ctxt' =
    1.78 +      let val elem' = map_ctxt_attrib Args.assignable (prep_facts ctxt' elem)
    1.79 +      in (elem', Context.proof_map (init elem') ctxt') end;
    1.80      val (elems, ctxt') = fold_map activate raw_elems ctxt;
    1.81    in (elems |> map (map_ctxt_attrib Args.closure), ctxt') end;
    1.82  
    1.83 -fun check_name name =
    1.84 -  if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name)
    1.85 -  else name;
    1.86 -
    1.87 -fun prep_facts prep_name get intern ctxt =
    1.88 +fun prep_facts ctxt =
    1.89    map_ctxt
    1.90 -   {binding = Binding.map_name prep_name,
    1.91 +   {binding = tap Name.of_binding,
    1.92      typ = I,
    1.93      term = I,
    1.94      pattern = I,
    1.95 -    fact = get ctxt,
    1.96 -    attrib = intern (ProofContext.theory_of ctxt)};
    1.97 +    fact = ProofContext.get_fact ctxt,
    1.98 +    attrib = Attrib.intern_src (ProofContext.theory_of ctxt)};
    1.99  
   1.100  in
   1.101  
   1.102 -fun activate x = gen_activate (prep_facts check_name ProofContext.get_fact Attrib.intern_src) x;
   1.103 +fun activate x = gen_activate prep_facts x;
   1.104  fun activate_i x = gen_activate (K I) x;
   1.105  
   1.106  end;

     2.1 --- a/src/Pure/Isar/locale.ML	Sun Mar 29 16:13:44 2009 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Sun Mar 29 17:47:50 2009 +0200
     2.3 @@ -293,52 +293,20 @@
     2.4  
     2.5  (** Public activation functions **)
     2.6  
     2.7 -local
     2.8 -
     2.9 -fun init_elem (Fixes fixes) (Context.Proof ctxt) =
    2.10 -      Context.Proof (ProofContext.add_fixes fixes ctxt |> snd)
    2.11 -  | init_elem (Assumes assms) (Context.Proof ctxt) =
    2.12 -      let
    2.13 -        val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms;
    2.14 -        val ctxt' = ctxt
    2.15 -          |> fold Variable.auto_fixes (maps (map fst o snd) assms')
    2.16 -          |> ProofContext.add_assms_i Assumption.assume_export assms' |> snd;
    2.17 -      in Context.Proof ctxt' end
    2.18 -  | init_elem (Defines defs) (Context.Proof ctxt) =
    2.19 -      let
    2.20 -        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
    2.21 -        val ctxt' = ctxt
    2.22 -          |> fold Variable.auto_fixes (map (fst o snd) defs')
    2.23 -          |> ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs')
    2.24 -          |> snd;
    2.25 -      in Context.Proof ctxt' end
    2.26 -  | init_elem (Notes (kind, facts)) (Context.Proof ctxt) =
    2.27 -      let
    2.28 -        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
    2.29 -      in Context.Proof (ProofContext.note_thmss kind facts' ctxt |> snd) end
    2.30 -  | init_elem (Notes (kind, facts)) (Context.Theory thy) =
    2.31 -      let
    2.32 -        val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
    2.33 -      in Context.Theory (PureThy.note_thmss kind facts' thy |> snd) end
    2.34 -  | init_elem _ (Context.Theory _) = raise Fail "Bad context element in global theory";
    2.35 -
    2.36 -in
    2.37 -
    2.38 -fun activate_declarations dep ctxt =
    2.39 +fun activate_declarations dep = Context.proof_map (fn context =>
    2.40    let
    2.41 -    val context = Context.Proof ctxt;
    2.42      val thy = Context.theory_of context;
    2.43      val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents;
    2.44 -  in Context.the_proof context' end;
    2.45 +  in context' end);
    2.46  
    2.47  fun activate_facts dep context =
    2.48    let
    2.49      val thy = Context.theory_of context;
    2.50 -    val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of) thy;
    2.51 +    val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy;
    2.52    in roundup thy activate dep (get_idents context, context) |-> put_idents end;
    2.53  
    2.54  fun init name thy =
    2.55 -  activate_all name thy init_elem (Element.transfer_morphism o Context.theory_of)
    2.56 +  activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
    2.57      ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
    2.58  
    2.59  fun print_locale thy show_facts raw_name =
    2.60 @@ -355,8 +323,6 @@
    2.61      |> Pretty.writeln
    2.62    end;
    2.63  
    2.64 -end;
    2.65 -
    2.66  
    2.67  (*** Registrations: interpretations in theories ***)
    2.68  
    2.69 @@ -398,7 +364,6 @@
    2.70    end;
    2.71  
    2.72  
    2.73 -
    2.74  (*** Storing results ***)
    2.75  
    2.76  (* Theorems *)