src/Pure/Isar/theory_target.ML
changeset 20915 dcb0a3e2f1bd
parent 20894 784eefc906aa
child 20962 e404275bff33
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Oct 09 02:20:07 2006 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Oct 09 02:20:08 2006 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  sig
     1.5    val init: xstring option -> theory -> local_theory
     1.6    val init_i: string option -> theory -> local_theory
     1.7 -  val exit: local_theory -> local_theory * theory
     1.8 -  val mapping: xstring option -> (local_theory -> local_theory) -> theory -> local_theory * theory
     1.9 +  val exit: local_theory -> Proof.context * theory
    1.10 +  val mapping: xstring option -> (local_theory -> local_theory) -> theory -> Proof.context * theory
    1.11  end;
    1.12  
    1.13  structure TheoryTarget: THEORY_TARGET =
    1.14 @@ -84,19 +84,17 @@
    1.15  
    1.16  in
    1.17  
    1.18 -fun axioms specs =
    1.19 -  fold (fold Variable.fix_frees o snd) specs #>   (* FIXME !? *)
    1.20 -  (fn lthy =>
    1.21 -    let
    1.22 -      val hyps = Assumption.assms_of lthy;
    1.23 -      fun axiom ((name, atts), props) thy = thy
    1.24 -        |> fold_map (add_axiom hyps) (PureThy.name_multi name props)
    1.25 -        |-> (fn ths => pair ((name, atts), [(ths, [])]));
    1.26 -    in
    1.27 -      lthy
    1.28 -      |> LocalTheory.theory_result (fold_map axiom specs)
    1.29 -      |-> LocalTheory.notes
    1.30 -    end);
    1.31 +fun axioms specs lthy =
    1.32 +  let
    1.33 +    val hyps = Assumption.assms_of lthy;
    1.34 +    fun axiom ((name, atts), props) thy = thy
    1.35 +      |> fold_map (add_axiom hyps) (PureThy.name_multi name props)
    1.36 +      |-> (fn ths => pair ((name, atts), [(ths, [])]));
    1.37 +  in
    1.38 +    lthy
    1.39 +    |> LocalTheory.theory_result (fold_map axiom specs)
    1.40 +    |-> LocalTheory.notes
    1.41 +  end;
    1.42  
    1.43  end;
    1.44  
    1.45 @@ -160,11 +158,11 @@
    1.46      ||> ProofContext.restore_naming lthy
    1.47    end;
    1.48  
    1.49 -fun theory_notes facts lthy = lthy |> LocalTheory.theory (fn thy =>
    1.50 +fun theory_notes keep_atts facts lthy = lthy |> LocalTheory.theory (fn thy =>
    1.51    let
    1.52      val facts' = facts
    1.53        |> Element.export_standard_facts lthy (ProofContext.init thy)
    1.54 -      |> Attrib.map_facts (Attrib.attribute_i thy);
    1.55 +      |> Attrib.map_facts (if keep_atts then Attrib.attribute_i thy else K I);
    1.56    in
    1.57      thy
    1.58      |> Sign.qualified_names
    1.59 @@ -175,8 +173,8 @@
    1.60  fun locale_notes loc facts lthy = lthy |> LocalTheory.target (fn ctxt =>
    1.61    #2 (Locale.add_thmss "" loc (Element.export_standard_facts lthy ctxt facts) ctxt));
    1.62  
    1.63 -fun notes "" facts = theory_notes facts #> context_notes facts
    1.64 -  | notes loc facts = locale_notes loc facts #> context_notes facts
    1.65 +fun notes "" facts = theory_notes true facts #> context_notes facts
    1.66 +  | notes loc facts = theory_notes false facts #> locale_notes loc facts #> context_notes facts;
    1.67  
    1.68  
    1.69  (* declarations *)
    1.70 @@ -191,22 +189,23 @@
    1.71  
    1.72  (* init and exit *)
    1.73  
    1.74 -fun target_operations loc : LocalTheory.operations =
    1.75 +fun target_operations loc exit : LocalTheory.operations =
    1.76   {pretty = pretty loc,
    1.77    consts = consts loc,
    1.78    axioms = axioms,
    1.79    defs = defs,
    1.80    notes = notes loc,
    1.81    term_syntax = term_syntax loc,
    1.82 -  declaration = declaration loc};
    1.83 +  declaration = declaration loc,
    1.84 +  exit = exit};
    1.85  
    1.86 -fun init_i NONE thy = LocalTheory.init (SOME "") (target_operations "") (ProofContext.init thy)
    1.87 +fun init_i NONE thy = LocalTheory.init (SOME "") (target_operations "" I) (ProofContext.init thy)
    1.88    | init_i (SOME loc) thy =
    1.89 -      LocalTheory.init (SOME (NameSpace.base loc)) (target_operations loc) (Locale.init loc thy);
    1.90 +      LocalTheory.init (SOME (NameSpace.base loc)) (target_operations loc I) (Locale.init loc thy);
    1.91  
    1.92  fun init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
    1.93  
    1.94 -fun exit lthy = (lthy, ProofContext.theory_of lthy);
    1.95 +val exit = LocalTheory.exit #> (fn lthy => (lthy, ProofContext.theory_of lthy));
    1.96  
    1.97  fun mapping loc f = init loc #> f #> exit;
    1.98