renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
authorwenzelm
Sat Mar 28 17:21:11 2009 +0100 (2009-03-28)
changeset 30761ac7570d80c3d
parent 30760 0fffc66b10d7
child 30762 cabf9ff3a129
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
src/HOL/Tools/function_package/fundef_package.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/element.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Pure/ML/ml_antiquote.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Mar 28 17:10:43 2009 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Mar 28 17:21:11 2009 +0100
     1.3 @@ -156,9 +156,9 @@
     1.4          val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
     1.5      in
     1.6        lthy
     1.7 -        |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
     1.8 -        |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
     1.9 -        |> ProofContext.note_thmss_i ""
    1.10 +        |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
    1.11 +        |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
    1.12 +        |> ProofContext.note_thmss ""
    1.13            [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
    1.14              [([Goal.norm_result termination], [])])] |> snd
    1.15          |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
     2.1 --- a/src/Pure/Isar/attrib.ML	Sat Mar 28 17:10:43 2009 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Sat Mar 28 17:21:11 2009 +0100
     2.3 @@ -123,7 +123,7 @@
     2.4  
     2.5  fun attribute thy = attribute_i thy o intern_src thy;
     2.6  
     2.7 -fun eval_thms ctxt args = ProofContext.note_thmss_i Thm.theoremK
     2.8 +fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
     2.9      [(Thm.empty_binding, args |> map (fn (a, atts) =>
    2.10          (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
    2.11    |> fst |> maps snd;
     3.1 --- a/src/Pure/Isar/element.ML	Sat Mar 28 17:10:43 2009 +0100
     3.2 +++ b/src/Pure/Isar/element.ML	Sat Mar 28 17:21:11 2009 +0100
     3.3 @@ -510,7 +510,7 @@
     3.4    | activate_elem (Notes (kind, facts)) ctxt =
     3.5        let
     3.6          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
     3.7 -        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
     3.8 +        val (res, ctxt') = ctxt |> ProofContext.note_thmss kind facts';
     3.9        in ctxt' end;
    3.10  
    3.11  fun gen_activate prep_facts raw_elems ctxt =
     4.1 --- a/src/Pure/Isar/locale.ML	Sat Mar 28 17:10:43 2009 +0100
     4.2 +++ b/src/Pure/Isar/locale.ML	Sat Mar 28 17:21:11 2009 +0100
     4.3 @@ -325,7 +325,7 @@
     4.4    | init_local_elem (Notes (kind, facts)) ctxt =
     4.5        let
     4.6          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
     4.7 -      in ProofContext.note_thmss_i kind facts' ctxt |> snd end
     4.8 +      in ProofContext.note_thmss kind facts' ctxt |> snd end
     4.9  
    4.10  fun cons_elem false (Notes notes) elems = elems
    4.11    | cons_elem _ elem elems = elem :: elems
     5.1 --- a/src/Pure/Isar/proof.ML	Sat Mar 28 17:10:43 2009 +0100
     5.2 +++ b/src/Pure/Isar/proof.ML	Sat Mar 28 17:21:11 2009 +0100
     5.3 @@ -623,7 +623,7 @@
     5.4  fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
     5.5    state
     5.6    |> assert_forward
     5.7 -  |> map_context_result (ProofContext.note_thmss_i ""
     5.8 +  |> map_context_result (ProofContext.note_thmss ""
     5.9      (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state)) args))
    5.10    |> these_factss (more_facts state)
    5.11    ||> opt_chain
    5.12 @@ -655,7 +655,7 @@
    5.13    state
    5.14    |> assert_backward
    5.15    |> map_context_result
    5.16 -    (ProofContext.note_thmss_i ""
    5.17 +    (ProofContext.note_thmss ""
    5.18        (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state))
    5.19          (no_binding args)))
    5.20    |> (fn (named_facts, state') =>
     6.1 --- a/src/Pure/Isar/proof_context.ML	Sat Mar 28 17:10:43 2009 +0100
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Mar 28 17:21:11 2009 +0100
     6.3 @@ -101,9 +101,7 @@
     6.4    val mandatory_path: string -> Proof.context -> Proof.context
     6.5    val restore_naming: Proof.context -> Proof.context -> Proof.context
     6.6    val reset_naming: Proof.context -> Proof.context
     6.7 -  val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
     6.8 -    Proof.context -> (string * thm list) list * Proof.context
     6.9 -  val note_thmss_i: string -> (Thm.binding * (thm list * attribute list) list) list ->
    6.10 +  val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
    6.11      Proof.context -> (string * thm list) list * Proof.context
    6.12    val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
    6.13    val read_vars: (binding * string option * mixfix) list -> Proof.context ->
    6.14 @@ -959,25 +957,23 @@
    6.15    | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
    6.16        (Facts.add_local do_props (naming_of ctxt) (b, ths) #> snd);
    6.17  
    6.18 -fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
    6.19 +in
    6.20 +
    6.21 +fun note_thmss kind = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
    6.22    let
    6.23      val pos = Binding.pos_of b;
    6.24      val name = full_name ctxt b;
    6.25      val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
    6.26  
    6.27 -    val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
    6.28 +    val facts = PureThy.name_thmss false pos name raw_facts;
    6.29      fun app (th, attrs) x =
    6.30 -      swap (Library.foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th));
    6.31 +      swap (Library.foldl_map
    6.32 +        (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
    6.33      val (res, ctxt') = fold_map app facts ctxt;
    6.34      val thms = PureThy.name_thms false false pos name (flat res);
    6.35      val Mode {stmt, ...} = get_mode ctxt;
    6.36    in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
    6.37  
    6.38 -in
    6.39 -
    6.40 -fun note_thmss k = gen_note_thmss get_fact k;
    6.41 -fun note_thmss_i k = gen_note_thmss (K I) k;
    6.42 -
    6.43  fun put_thms do_props thms ctxt = ctxt
    6.44    |> map_naming (K local_naming)
    6.45    |> ContextPosition.set_visible false
    6.46 @@ -1161,7 +1157,7 @@
    6.47    in
    6.48      ctxt2
    6.49      |> auto_bind_facts (flat propss)
    6.50 -    |> note_thmss_i Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
    6.51 +    |> note_thmss Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
    6.52    end;
    6.53  
    6.54  in
     7.1 --- a/src/Pure/Isar/specification.ML	Sat Mar 28 17:10:43 2009 +0100
     7.2 +++ b/src/Pure/Isar/specification.ML	Sat Mar 28 17:21:11 2009 +0100
     7.3 @@ -327,7 +327,7 @@
     7.4          val (facts, goal_ctxt) = elems_ctxt
     7.5            |> (snd o ProofContext.add_fixes_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
     7.6            |> fold_map assume_case (obtains ~~ propp)
     7.7 -          |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
     7.8 +          |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
     7.9                  [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
    7.10        in ((prems, stmt, facts), goal_ctxt) end);
    7.11  
    7.12 @@ -370,7 +370,7 @@
    7.13        end;
    7.14    in
    7.15      goal_ctxt
    7.16 -    |> ProofContext.note_thmss_i Thm.assumptionK
    7.17 +    |> ProofContext.note_thmss Thm.assumptionK
    7.18        [((Binding.name AutoBind.assmsN, []), [(prems, [])])]
    7.19      |> snd
    7.20      |> Proof.theorem_i before_qed after_qed' (map snd stmt)
     8.1 --- a/src/Pure/Isar/theory_target.ML	Sat Mar 28 17:10:43 2009 +0100
     8.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Mar 28 17:21:11 2009 +0100
     8.3 @@ -160,9 +160,9 @@
     8.4    in
     8.5      lthy |> LocalTheory.theory
     8.6        (PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd)
     8.7 -    |> not is_locale ? LocalTheory.target (ProofContext.note_thmss_i kind global_facts #> snd)
     8.8 +    |> not is_locale ? LocalTheory.target (ProofContext.note_thmss kind global_facts #> snd)
     8.9      |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
    8.10 -    |> ProofContext.note_thmss_i kind local_facts
    8.11 +    |> ProofContext.note_thmss kind local_facts
    8.12    end;
    8.13  
    8.14  
     9.1 --- a/src/Pure/ML/ml_antiquote.ML	Sat Mar 28 17:10:43 2009 +0100
     9.2 +++ b/src/Pure/ML/ml_antiquote.ML	Sat Mar 28 17:21:11 2009 +0100
     9.3 @@ -87,7 +87,7 @@
     9.4  val _ = macro "note" (Args.context :|-- (fn ctxt =>
     9.5    P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
     9.6      ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
     9.7 -  >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt))));
     9.8 +  >> (fn args => #2 (ProofContext.note_thmss "" args ctxt))));
     9.9  
    9.10  val _ = value "ctyp" (Args.typ >> (fn T =>
    9.11    "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));