eliminated obsolete "internal" kind -- collapsed to unspecific "";
authorwenzelm
Thu Nov 12 22:02:11 2009 +0100 (2009-11-12)
changeset 33643b275f26a638b
parent 33642 d983509dbf31
child 33644 5266a72e0889
eliminated obsolete "internal" kind -- collapsed to unspecific "";
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/recdef.ML
src/Pure/General/markup.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof_display.ML
src/Pure/drule.ML
src/Pure/more_thm.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Nov 12 21:59:35 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Nov 12 22:02:11 2009 +0100
     1.3 @@ -569,7 +569,7 @@
     1.4        thy3
     1.5        |> Sign.map_naming Name_Space.conceal
     1.6        |> Inductive.add_inductive_global (serial ())
     1.7 -          {quiet_mode = false, verbose = false, kind = Thm.internalK,
     1.8 +          {quiet_mode = false, verbose = false, kind = "",
     1.9             alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
    1.10             skip_mono = true, fork_mono = false}
    1.11            (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
    1.12 @@ -1513,7 +1513,7 @@
    1.13        thy10
    1.14        |> Sign.map_naming Name_Space.conceal
    1.15        |> Inductive.add_inductive_global (serial ())
    1.16 -          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
    1.17 +          {quiet_mode = #quiet config, verbose = false, kind = "",
    1.18             alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
    1.19             skip_mono = true, fork_mono = false}
    1.20            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
     2.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Nov 12 21:59:35 2009 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Nov 12 22:02:11 2009 +0100
     2.3 @@ -156,7 +156,7 @@
     2.4        thy0
     2.5        |> Sign.map_naming Name_Space.conceal
     2.6        |> Inductive.add_inductive_global (serial ())
     2.7 -          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
     2.8 +          {quiet_mode = #quiet config, verbose = false, kind = "",
     2.9              alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
    2.10              skip_mono = true, fork_mono = false}
    2.11            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
     3.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Thu Nov 12 21:59:35 2009 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Thu Nov 12 22:02:11 2009 +0100
     3.3 @@ -175,7 +175,7 @@
     3.4        thy1
     3.5        |> Sign.map_naming Name_Space.conceal
     3.6        |> Inductive.add_inductive_global (serial ())
     3.7 -          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
     3.8 +          {quiet_mode = #quiet config, verbose = false, kind = "",
     3.9             alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
    3.10             skip_mono = true, fork_mono = false}
    3.11            (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
     4.1 --- a/src/HOL/Tools/Function/function_core.ML	Thu Nov 12 21:59:35 2009 +0100
     4.2 +++ b/src/HOL/Tools/Function/function_core.ML	Thu Nov 12 22:02:11 2009 +0100
     4.3 @@ -460,7 +460,7 @@
     4.4        |> Inductive.add_inductive_i
     4.5            {quiet_mode = true,
     4.6              verbose = ! trace,
     4.7 -            kind = Thm.internalK,
     4.8 +            kind = "",
     4.9              alt_name = Binding.empty,
    4.10              coind = false,
    4.11              no_elim = false,
    4.12 @@ -519,7 +519,7 @@
    4.13          $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
    4.14        |> Syntax.check_term lthy
    4.15    in
    4.16 -    LocalTheory.define Thm.internalK
    4.17 +    LocalTheory.define ""
    4.18        ((Binding.name (function_name fname), mixfix),
    4.19          ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
    4.20    end
     5.1 --- a/src/HOL/Tools/Function/mutual.ML	Thu Nov 12 21:59:35 2009 +0100
     5.2 +++ b/src/HOL/Tools/Function/mutual.ML	Thu Nov 12 22:02:11 2009 +0100
     5.3 @@ -146,7 +146,7 @@
     5.4        fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
     5.5            let
     5.6              val ((f, (_, f_defthm)), lthy') =
     5.7 -              LocalTheory.define Thm.internalK
     5.8 +              LocalTheory.define ""
     5.9                  ((Binding.name fname, mixfix),
    5.10                    ((Binding.conceal (Binding.name (fname ^ "_def")), []),
    5.11                    Term.subst_bound (fsum, f_def))) lthy
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Nov 12 21:59:35 2009 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Nov 12 22:02:11 2009 +0100
     6.3 @@ -355,7 +355,7 @@
     6.4                thy
     6.5                |> Sign.map_naming Name_Space.conceal
     6.6                |> Inductive.add_inductive_global (serial ())
     6.7 -                {quiet_mode = false, verbose = false, kind = Thm.internalK,
     6.8 +                {quiet_mode = false, verbose = false, kind = "",
     6.9                    alt_name = Binding.empty, coind = false, no_elim = false,
    6.10                    no_ind = false, skip_mono = false, fork_mono = false}
    6.11                  (map (fn (s, T) =>
     7.1 --- a/src/HOL/Tools/inductive.ML	Thu Nov 12 21:59:35 2009 +0100
     7.2 +++ b/src/HOL/Tools/inductive.ML	Thu Nov 12 22:02:11 2009 +0100
     7.3 @@ -663,7 +663,7 @@
     7.4  
     7.5      val ((rec_const, (_, fp_def)), lthy') = lthy
     7.6        |> LocalTheory.conceal
     7.7 -      |> LocalTheory.define Thm.internalK
     7.8 +      |> LocalTheory.define ""
     7.9          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
    7.10           ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
    7.11           fold_rev lambda params
    7.12 @@ -686,13 +686,13 @@
    7.13            end) (cnames_syn ~~ cs);
    7.14      val (consts_defs, lthy'') = lthy'
    7.15        |> LocalTheory.conceal
    7.16 -      |> fold_map (LocalTheory.define Thm.internalK) specs
    7.17 +      |> fold_map (LocalTheory.define "") specs
    7.18        ||> LocalTheory.restore_naming lthy';
    7.19      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
    7.20  
    7.21      val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'';
    7.22      val ((_, [mono']), lthy''') =
    7.23 -      LocalTheory.note Thm.internalK (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
    7.24 +      LocalTheory.note "" (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
    7.25  
    7.26    in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
    7.27      list_comb (rec_const, params), preds, argTs, bs, xs)
     8.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Nov 12 21:59:35 2009 +0100
     8.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Nov 12 22:02:11 2009 +0100
     8.3 @@ -485,7 +485,7 @@
     8.4      (* define inductive sets using previously defined predicates *)
     8.5      val (defs, lthy2) = lthy1
     8.6        |> LocalTheory.conceal  (* FIXME ?? *)
     8.7 -      |> fold_map (LocalTheory.define Thm.internalK)
     8.8 +      |> fold_map (LocalTheory.define "")
     8.9          (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
    8.10             fold_rev lambda params (HOLogic.Collect_const U $
    8.11               HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
     9.1 --- a/src/HOL/Tools/recdef.ML	Thu Nov 12 21:59:35 2009 +0100
     9.2 +++ b/src/HOL/Tools/recdef.ML	Thu Nov 12 22:02:11 2009 +0100
     9.3 @@ -263,7 +263,7 @@
     9.4        error ("No termination condition #" ^ string_of_int i ^
     9.5          " in recdef definition of " ^ quote name);
     9.6    in
     9.7 -    Specification.theorem Thm.internalK NONE (K I)
     9.8 +    Specification.theorem "" NONE (K I)
     9.9        (Binding.conceal (Binding.name bname), atts) []
    9.10        (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
    9.11    end;
    10.1 --- a/src/Pure/General/markup.ML	Thu Nov 12 21:59:35 2009 +0100
    10.2 +++ b/src/Pure/General/markup.ML	Thu Nov 12 22:02:11 2009 +0100
    10.3 @@ -14,7 +14,6 @@
    10.4    val name: string -> T -> T
    10.5    val bindingN: string val binding: string -> T
    10.6    val kindN: string
    10.7 -  val internalK: string
    10.8    val entityN: string val entity: string -> T
    10.9    val defN: string
   10.10    val refN: string
   10.11 @@ -154,8 +153,6 @@
   10.12  
   10.13  val kindN = "kind";
   10.14  
   10.15 -val internalK = "internal";
   10.16 -
   10.17  
   10.18  (* formal entities *)
   10.19  
    11.1 --- a/src/Pure/Isar/expression.ML	Thu Nov 12 21:59:35 2009 +0100
    11.2 +++ b/src/Pure/Isar/expression.ML	Thu Nov 12 22:02:11 2009 +0100
    11.3 @@ -682,7 +682,7 @@
    11.4            val (_, thy'') =
    11.5              thy'
    11.6              |> Sign.mandatory_path (Binding.name_of abinding)
    11.7 -            |> PureThy.note_thmss Thm.internalK
    11.8 +            |> PureThy.note_thmss ""
    11.9                [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
   11.10              ||> Sign.restore_naming thy';
   11.11            in (SOME statement, SOME intro, axioms, thy'') end;
   11.12 @@ -696,7 +696,7 @@
   11.13            val (_, thy'''') =
   11.14              thy'''
   11.15              |> Sign.mandatory_path (Binding.name_of binding)
   11.16 -            |> PureThy.note_thmss Thm.internalK
   11.17 +            |> PureThy.note_thmss ""
   11.18                   [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
   11.19                    ((Binding.conceal (Binding.name axiomsN), []),
   11.20                      [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
   11.21 @@ -755,7 +755,7 @@
   11.22  
   11.23      val notes =
   11.24        if is_some asm then
   11.25 -        [(Thm.internalK, [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
   11.26 +        [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
   11.27            [([Assumption.assume (cterm_of thy' (the asm))],
   11.28              [(Attrib.internal o K) Locale.witness_add])])])]
   11.29        else [];
    12.1 --- a/src/Pure/Isar/locale.ML	Thu Nov 12 21:59:35 2009 +0100
    12.2 +++ b/src/Pure/Isar/locale.ML	Thu Nov 12 22:02:11 2009 +0100
    12.3 @@ -518,7 +518,7 @@
    12.4  
    12.5  fun add_decls add loc decl =
    12.6    ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
    12.7 -  add_thmss loc Thm.internalK
    12.8 +  add_thmss loc ""
    12.9      [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
   12.10        [([Drule.dummy_thm], [])])];
   12.11  
    13.1 --- a/src/Pure/Isar/proof_display.ML	Thu Nov 12 21:59:35 2009 +0100
    13.2 +++ b/src/Pure/Isar/proof_display.ML	Thu Nov 12 22:02:11 2009 +0100
    13.3 @@ -91,7 +91,7 @@
    13.4  in
    13.5  
    13.6  fun print_results do_print ctxt ((kind, name), facts) =
    13.7 -  if not do_print orelse kind = "" orelse kind = Thm.internalK then ()
    13.8 +  if not do_print orelse kind = "" then ()
    13.9    else if name = "" then
   13.10      Pretty.writeln (Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
   13.11    else Pretty.writeln
    14.1 --- a/src/Pure/drule.ML	Thu Nov 12 21:59:35 2009 +0100
    14.2 +++ b/src/Pure/drule.ML	Thu Nov 12 22:02:11 2009 +0100
    14.3 @@ -710,13 +710,11 @@
    14.4  
    14.5  val protectI =
    14.6    store_thm (Binding.conceal (Binding.name "protectI"))
    14.7 -    (Thm.kind_rule Thm.internalK (standard
    14.8 -      (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
    14.9 +    (standard (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)));
   14.10  
   14.11  val protectD =
   14.12    store_thm (Binding.conceal (Binding.name "protectD"))
   14.13 -    (Thm.kind_rule Thm.internalK (standard
   14.14 -      (Thm.equal_elim prop_def (Thm.assume (protect A)))));
   14.15 +    (standard (Thm.equal_elim prop_def (Thm.assume (protect A))));
   14.16  
   14.17  val protect_cong =
   14.18    store_standard_thm_open (Binding.name "protect_cong") (Thm.reflexive (protect A));
   14.19 @@ -734,8 +732,7 @@
   14.20  
   14.21  val termI =
   14.22    store_thm (Binding.conceal (Binding.name "termI"))
   14.23 -    (Thm.kind_rule Thm.internalK (standard
   14.24 -      (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
   14.25 +    (standard (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))));
   14.26  
   14.27  fun mk_term ct =
   14.28    let
   14.29 @@ -764,15 +761,14 @@
   14.30  
   14.31  val sort_constraintI =
   14.32    store_thm (Binding.conceal (Binding.name "sort_constraintI"))
   14.33 -    (Thm.kind_rule Thm.internalK (standard
   14.34 -      (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T))));
   14.35 +    (standard (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T)));
   14.36  
   14.37  val sort_constraint_eq =
   14.38    store_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
   14.39 -    (Thm.kind_rule Thm.internalK (standard
   14.40 +    (standard
   14.41        (Thm.equal_intr
   14.42          (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
   14.43 -        (implies_intr_list [A, C] (Thm.assume A)))));
   14.44 +        (implies_intr_list [A, C] (Thm.assume A))));
   14.45  
   14.46  end;
   14.47  
    15.1 --- a/src/Pure/more_thm.ML	Thu Nov 12 21:59:35 2009 +0100
    15.2 +++ b/src/Pure/more_thm.ML	Thu Nov 12 22:02:11 2009 +0100
    15.3 @@ -91,7 +91,6 @@
    15.4    val generatedK : string
    15.5    val lemmaK: string
    15.6    val corollaryK: string
    15.7 -  val internalK: string
    15.8    val get_kind: thm -> string
    15.9    val kind_rule: string -> thm -> thm
   15.10    val kind: string -> attribute
   15.11 @@ -421,7 +420,6 @@
   15.12  val generatedK = "generatedK"
   15.13  val lemmaK = "lemma";
   15.14  val corollaryK = "corollary";
   15.15 -val internalK = Markup.internalK;
   15.16  
   15.17  fun get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
   15.18