moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
authorwenzelm
Thu Aug 14 16:52:46 2008 +0200 (2008-08-14)
changeset 2786527a8ad9612a3
parent 27864 827730aea9e8
child 27866 c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
src/HOL/Import/shuffler.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/ex/Quickcheck.thy
src/Pure/Isar/attrib.ML
src/Pure/Isar/element.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Proof/extraction.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Thy/thm_deps.ML
src/Pure/axclass.ML
src/Pure/drule.ML
src/Pure/meta_simplifier.ML
src/Pure/pure_thy.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu Aug 14 11:55:05 2008 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu Aug 14 16:52:46 2008 +0200
     1.3 @@ -627,7 +627,7 @@
     1.4          val shuffles = ShuffleData.get thy
     1.5          val ignored = collect_ignored shuffles []
     1.6          val all_thms =
     1.7 -          map (`PureThy.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
     1.8 +          map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
     1.9      in
    1.10          List.filter (match_consts ignored t) all_thms
    1.11      end
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Aug 14 11:55:05 2008 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Aug 14 16:52:46 2008 +0200
     2.3 @@ -217,7 +217,7 @@
     2.4        [(("", nth inducts index), [Induct.induct_type name]),
     2.5         (("", exhaustion), [Induct.cases_type name])];
     2.6      fun unnamed_rule i =
     2.7 -      (("", nth inducts i), [PureThy.kind_internal, Induct.induct_type ""]);
     2.8 +      (("", nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
     2.9    in
    2.10      thy |> PureThy.add_thms
    2.11        (maps named_rules infos @
     3.1 --- a/src/HOL/Tools/meson.ML	Thu Aug 14 11:55:05 2008 +0200
     3.2 +++ b/src/HOL/Tools/meson.ML	Thu Aug 14 16:52:46 2008 +0200
     3.3 @@ -431,7 +431,7 @@
     3.4  (*Use "theorem naming" to label the clauses*)
     3.5  fun name_thms label =
     3.6      let fun name1 (th, (k,ths)) =
     3.7 -          (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths)
     3.8 +          (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
     3.9      in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
    3.10  
    3.11  (*Is the given disjunction an all-negative support clause?*)
     4.1 --- a/src/HOL/Tools/metis_tools.ML	Thu Aug 14 11:55:05 2008 +0200
     4.2 +++ b/src/HOL/Tools/metis_tools.ML	Thu Aug 14 16:52:46 2008 +0200
     4.3 @@ -568,7 +568,7 @@
     4.4    (* Main function to start metis prove and reconstruction *)
     4.5    fun FOL_SOLVE mode ctxt cls ths0 =
     4.6      let val thy = ProofContext.theory_of ctxt
     4.7 -        val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
     4.8 +        val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
     4.9          val ths = List.concat (map #2 th_cls_pairs)
    4.10          val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
    4.11                  else ();
     5.1 --- a/src/HOL/Tools/res_atp.ML	Thu Aug 14 11:55:05 2008 +0200
     5.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Aug 14 16:52:46 2008 +0200
     5.3 @@ -817,7 +817,7 @@
     5.4  fun sledgehammer state =
     5.5    let
     5.6      val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state)
     5.7 -    val chain_ths = map (PureThy.put_name_hint Recon.chained_hint) chain_ths
     5.8 +    val chain_ths = map (Thm.put_name_hint Recon.chained_hint) chain_ths
     5.9                      (*Mark the chained theorems to keep them out of metis calls;
    5.10                        their original "name hints" may be bad anyway.*)
    5.11      val thy = ProofContext.theory_of ctxt
     6.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Aug 14 11:55:05 2008 +0200
     6.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Aug 14 16:52:46 2008 +0200
     6.3 @@ -327,7 +327,7 @@
     6.4      | _ => false;
     6.5  
     6.6  fun bad_for_atp th =
     6.7 -  PureThy.is_internal th
     6.8 +  Thm.is_internal th
     6.9    orelse too_complex (prop_of th)
    6.10    orelse exists_type type_has_empty_sort (prop_of th)
    6.11    orelse is_strange_thm th;
    6.12 @@ -340,11 +340,11 @@
    6.13  fun flatten_name s = space_implode "_X" (NameSpace.explode s);
    6.14  
    6.15  fun fake_name th =
    6.16 -  if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th)
    6.17 +  if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
    6.18    else gensym "unknown_thm_";
    6.19  
    6.20  fun name_or_string th =
    6.21 -  if PureThy.has_name_hint th then PureThy.get_name_hint th
    6.22 +  if Thm.has_name_hint th then Thm.get_name_hint th
    6.23    else Display.string_of_thm th;
    6.24  
    6.25  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
    6.26 @@ -404,7 +404,7 @@
    6.27  
    6.28  (**** Extract and Clausify theorems from a theory's claset and simpset ****)
    6.29  
    6.30 -fun pairname th = (PureThy.get_name_hint th, th);
    6.31 +fun pairname th = (Thm.get_name_hint th, th);
    6.32  
    6.33  fun rules_of_claset cs =
    6.34    let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
     7.1 --- a/src/HOL/Tools/res_reconstruct.ML	Thu Aug 14 11:55:05 2008 +0200
     7.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Thu Aug 14 16:52:46 2008 +0200
     7.3 @@ -488,7 +488,7 @@
     7.4  
     7.5  (**** retrieve the axioms that were used in the proof ****)
     7.6  
     7.7 -(*PureThy.get_name_hint returns "??.unknown" if no name is available.*)
     7.8 +(*Thm.get_name_hint returns "??.unknown" if no name is available.*)
     7.9  fun goodhint x = (x <> "??.unknown");  
    7.10  
    7.11  (*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)
     8.1 --- a/src/HOL/ex/Quickcheck.thy	Thu Aug 14 11:55:05 2008 +0200
     8.2 +++ b/src/HOL/ex/Quickcheck.thy	Thu Aug 14 16:52:46 2008 +0200
     8.3 @@ -121,7 +121,7 @@
     8.4                  |> singleton (ProofContext.export lthy (ProofContext.init thy))
     8.5              in
     8.6                lthy
     8.7 -              |> LocalTheory.theory (PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [PureThy.kind_internal])
     8.8 +              |> LocalTheory.theory (PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal])
     8.9                     #-> Code.add_func)
    8.10              end;
    8.11          in
     9.1 --- a/src/Pure/Isar/attrib.ML	Thu Aug 14 11:55:05 2008 +0200
     9.2 +++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 16:52:46 2008 +0200
     9.3 @@ -215,10 +215,10 @@
     9.4  
     9.5  (* tags *)
     9.6  
     9.7 -val tagged = syntax (Scan.lift (Args.name -- Args.name) >> PureThy.tag);
     9.8 -val untagged = syntax (Scan.lift Args.name >> PureThy.untag);
     9.9 +val tagged = syntax (Scan.lift (Args.name -- Args.name) >> Thm.tag);
    9.10 +val untagged = syntax (Scan.lift Args.name >> Thm.untag);
    9.11  
    9.12 -val kind = syntax (Scan.lift Args.name >> PureThy.kind);
    9.13 +val kind = syntax (Scan.lift Args.name >> Thm.kind);
    9.14  
    9.15  
    9.16  (* rule composition *)
    10.1 --- a/src/Pure/Isar/element.ML	Thu Aug 14 11:55:05 2008 +0200
    10.2 +++ b/src/Pure/Isar/element.ML	Thu Aug 14 16:52:46 2008 +0200
    10.3 @@ -228,9 +228,9 @@
    10.4  
    10.5  fun thm_name kind th prts =
    10.6    let val head =
    10.7 -    if PureThy.has_name_hint th then
    10.8 +    if Thm.has_name_hint th then
    10.9        Pretty.block [Pretty.command kind,
   10.10 -        Pretty.brk 1, Pretty.str (Sign.base_name (PureThy.get_name_hint th) ^ ":")]
   10.11 +        Pretty.brk 1, Pretty.str (Sign.base_name (Thm.get_name_hint th) ^ ":")]
   10.12      else Pretty.command kind
   10.13    in Pretty.block (Pretty.fbreaks (head :: prts)) end;
   10.14  
    11.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 14 11:55:05 2008 +0200
    11.2 +++ b/src/Pure/Isar/locale.ML	Thu Aug 14 16:52:46 2008 +0200
    11.3 @@ -1775,7 +1775,7 @@
    11.4        |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
    11.5        |> Sign.declare_const [] (bname, predT, NoSyn) |> snd
    11.6        |> PureThy.add_defs false
    11.7 -        [((Thm.def_name bname, Logic.mk_equals (head, body)), [PureThy.kind_internal])];
    11.8 +        [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
    11.9      val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
   11.10  
   11.11      val cert = Thm.cterm_of defs_thy;
    12.1 --- a/src/Pure/Isar/rule_cases.ML	Thu Aug 14 11:55:05 2008 +0200
    12.2 +++ b/src/Pure/Isar/rule_cases.ML	Thu Aug 14 16:52:46 2008 +0200
    12.3 @@ -223,8 +223,8 @@
    12.4  
    12.5  fun put_consumes NONE th = th
    12.6    | put_consumes (SOME n) th = th
    12.7 -      |> PureThy.untag_rule consumes_tagN
    12.8 -      |> PureThy.tag_rule
    12.9 +      |> Thm.untag_rule consumes_tagN
   12.10 +      |> Thm.tag_rule
   12.11          (consumes_tagN, Library.string_of_int (if n < 0 then Thm.nprems_of th + n else n));
   12.12  
   12.13  fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
   12.14 @@ -247,8 +247,8 @@
   12.15  
   12.16  fun add_case_names NONE = I
   12.17    | add_case_names (SOME names) =
   12.18 -      PureThy.untag_rule case_names_tagN
   12.19 -      #> PureThy.tag_rule (case_names_tagN, implode_args names);
   12.20 +      Thm.untag_rule case_names_tagN
   12.21 +      #> Thm.tag_rule (case_names_tagN, implode_args names);
   12.22  
   12.23  fun lookup_case_names th =
   12.24    AList.lookup (op =) (Thm.get_tags th) case_names_tagN
    13.1 --- a/src/Pure/Proof/extraction.ML	Thu Aug 14 11:55:05 2008 +0200
    13.2 +++ b/src/Pure/Proof/extraction.ML	Thu Aug 14 16:52:46 2008 +0200
    13.3 @@ -356,7 +356,7 @@
    13.4      val is_def =
    13.5        (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
    13.6           (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts)
    13.7 -           andalso (PureThy.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
    13.8 +           andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
    13.9         | _ => false) handle TERM _ => false;
   13.10    in
   13.11      (ExtractionData.put (if is_def then
    14.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Aug 14 11:55:05 2008 +0200
    14.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Aug 14 16:52:46 2008 +0200
    14.3 @@ -176,7 +176,7 @@
    14.4  fun tell_thm_deps ths =
    14.5    if print_mode_active thm_depsN then
    14.6      let
    14.7 -      val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths);
    14.8 +      val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
    14.9        val deps = Symtab.keys (fold Proofterm.thms_of_proof'
   14.10  				   (map Thm.proof_of ths) Symtab.empty);
   14.11      in
    15.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 14 11:55:05 2008 +0200
    15.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 14 16:52:46 2008 +0200
    15.3 @@ -341,7 +341,7 @@
    15.4  fun tell_thm_deps ths =
    15.5    if !show_theorem_dependencies then
    15.6        let
    15.7 -        val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths);
    15.8 +        val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
    15.9          val deps = (Symtab.keys (fold Proofterm.thms_of_proof'
   15.10                                          (map Thm.proof_of ths) Symtab.empty))
   15.11        in
    16.1 --- a/src/Pure/Thy/thm_deps.ML	Thu Aug 14 11:55:05 2008 +0200
    16.2 +++ b/src/Pure/Thy/thm_deps.ML	Thu Aug 14 16:52:46 2008 +0200
    16.3 @@ -93,13 +93,13 @@
    16.4        | SOME ps => not (member (op aconv) (map fst ps) (Thm.prop_of th));
    16.5      (* groups containing at least one used theorem *)
    16.6      val grps = fold (fn p as (_, thm) => if is_unused p then I else
    16.7 -      case PureThy.get_group thm of
    16.8 +      case Thm.get_group thm of
    16.9          NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
   16.10      val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
   16.11 -      if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (PureThy.get_kind thm)
   16.12 +      if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
   16.13          andalso is_unused p
   16.14        then
   16.15 -        (case PureThy.get_group thm of
   16.16 +        (case Thm.get_group thm of
   16.17             NONE => (p :: thms, grps')
   16.18           | SOME grp =>
   16.19               (* do not output theorem if another theorem in group has been used *)
    17.1 --- a/src/Pure/axclass.ML	Thu Aug 14 11:55:05 2008 +0200
    17.2 +++ b/src/Pure/axclass.ML	Thu Aug 14 16:52:46 2008 +0200
    17.3 @@ -374,7 +374,7 @@
    17.4            (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
    17.5      #>> Thm.varifyT
    17.6      #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
    17.7 -    #> PureThy.add_thm ((c', thm), [PureThy.kind_internal])
    17.8 +    #> PureThy.add_thm ((c', thm), [Thm.kind_internal])
    17.9      #> snd
   17.10      #> Sign.restore_naming thy
   17.11      #> pair (Const (c, T))))
    18.1 --- a/src/Pure/drule.ML	Thu Aug 14 11:55:05 2008 +0200
    18.2 +++ b/src/Pure/drule.ML	Thu Aug 14 16:52:46 2008 +0200
    18.3 @@ -791,13 +791,13 @@
    18.4    val term_def = get_axiom "term_def";
    18.5  in
    18.6    val protect = Thm.capply (certify Logic.protectC);
    18.7 -  val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard
    18.8 +  val protectI = store_thm "protectI" (Thm.kind_rule Thm.internalK (standard
    18.9        (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
   18.10 -  val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard
   18.11 +  val protectD = store_thm "protectD" (Thm.kind_rule Thm.internalK (standard
   18.12        (Thm.equal_elim prop_def (Thm.assume (protect A)))));
   18.13    val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A));
   18.14  
   18.15 -  val termI = store_thm "termI" (PureThy.kind_rule Thm.internalK (standard
   18.16 +  val termI = store_thm "termI" (Thm.kind_rule Thm.internalK (standard
   18.17        (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
   18.18  end;
   18.19  
    19.1 --- a/src/Pure/meta_simplifier.ML	Thu Aug 14 11:55:05 2008 +0200
    19.2 +++ b/src/Pure/meta_simplifier.ML	Thu Aug 14 16:52:46 2008 +0200
    19.3 @@ -528,7 +528,7 @@
    19.4    end;
    19.5  
    19.6  fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
    19.7 -  maps (fn thm => map (rpair (PureThy.get_name_hint thm)) (mk thm)) thms;
    19.8 +  maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk thm)) thms;
    19.9  
   19.10  fun extract_safe_rrules (ss, thm) =
   19.11    maps (orient_rrule ss) (extract_rews (ss, [thm]));
    20.1 --- a/src/Pure/pure_thy.ML	Thu Aug 14 11:55:05 2008 +0200
    20.2 +++ b/src/Pure/pure_thy.ML	Thu Aug 14 16:52:46 2008 +0200
    20.3 @@ -7,23 +7,6 @@
    20.4  
    20.5  signature PURE_THY =
    20.6  sig
    20.7 -  val tag_rule: Markup.property -> thm -> thm
    20.8 -  val untag_rule: string -> thm -> thm
    20.9 -  val tag: Markup.property -> attribute
   20.10 -  val untag: string -> attribute
   20.11 -  val has_name_hint: thm -> bool
   20.12 -  val get_name_hint: thm -> string
   20.13 -  val put_name_hint: string -> thm -> thm
   20.14 -  val get_group: thm -> string option
   20.15 -  val put_group: string -> thm -> thm
   20.16 -  val group: string -> attribute
   20.17 -  val has_kind: thm -> bool
   20.18 -  val get_kind: thm -> string
   20.19 -  val kind_rule: string -> thm -> thm
   20.20 -  val kind: string -> attribute
   20.21 -  val kind_internal: attribute
   20.22 -  val has_internal: Markup.property list -> bool
   20.23 -  val is_internal: thm -> bool
   20.24    val facts_of: theory -> Facts.T
   20.25    val intern_fact: theory -> xstring -> string
   20.26    val defined_fact: theory -> string -> bool
   20.27 @@ -69,52 +52,6 @@
   20.28  struct
   20.29  
   20.30  
   20.31 -(*** theorem tags ***)
   20.32 -
   20.33 -(* add / delete tags *)
   20.34 -
   20.35 -fun tag_rule tg = Thm.map_tags (insert (op =) tg);
   20.36 -fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s'));
   20.37 -
   20.38 -fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x;
   20.39 -fun untag s x = Thm.rule_attribute (K (untag_rule s)) x;
   20.40 -
   20.41 -
   20.42 -(* unofficial theorem names *)
   20.43 -
   20.44 -fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN);
   20.45 -
   20.46 -val has_name_hint = can the_name_hint;
   20.47 -val get_name_hint = the_default "??.unknown" o try the_name_hint;
   20.48 -
   20.49 -fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name);
   20.50 -
   20.51 -
   20.52 -(* theorem groups *)
   20.53 -
   20.54 -fun get_group thm = AList.lookup (op =) (Thm.get_tags thm) Markup.groupN;
   20.55 -
   20.56 -fun put_group name =
   20.57 -  if name = "" then I else Thm.map_tags (AList.update (op =) (Markup.groupN, name));
   20.58 -
   20.59 -fun group name = Thm.rule_attribute (K (put_group name));
   20.60 -
   20.61 -
   20.62 -(* theorem kinds *)
   20.63 -
   20.64 -fun the_kind thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.kindN);
   20.65 -
   20.66 -val has_kind = can the_kind;
   20.67 -val get_kind = the_default "" o try the_kind;
   20.68 -
   20.69 -fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;
   20.70 -fun kind k x = if k = "" then x else Thm.rule_attribute (K (kind_rule k)) x;
   20.71 -fun kind_internal x = kind Thm.internalK x;
   20.72 -fun has_internal tags = exists (fn tg => tg = (Markup.kindN, Thm.internalK)) tags;
   20.73 -val is_internal = has_internal o Thm.get_tags;
   20.74 -
   20.75 -
   20.76 -
   20.77  (*** stored facts ***)
   20.78  
   20.79  (** theory data **)
   20.80 @@ -159,7 +96,7 @@
   20.81  fun get_thm thy name = Facts.the_single name (get_thms thy name);
   20.82  
   20.83  fun all_thms_of thy =
   20.84 -  Facts.fold_static (fn (_, ths) => append (map (`(get_name_hint)) ths)) (facts_of thy) [];
   20.85 +  Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
   20.86  
   20.87  
   20.88  
   20.89 @@ -180,8 +117,8 @@
   20.90  
   20.91  fun name_thm pre official name thm = thm
   20.92    |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)
   20.93 -  |> (if has_name_hint thm andalso pre orelse name = "" then I else put_name_hint name)
   20.94 -  |> Thm.map_tags (Position.default_properties (Position.thread_data ()));
   20.95 +  |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name)
   20.96 +  |> Thm.default_position (Position.thread_data ());
   20.97  
   20.98  fun name_thms pre official name xs =
   20.99    map (uncurry (name_thm pre official)) (name_multi name xs);
  20.100 @@ -250,8 +187,8 @@
  20.101  
  20.102  in
  20.103  
  20.104 -fun note_thmss k = gen_note_thmss (kind k);
  20.105 -fun note_thmss_grouped k g = gen_note_thmss (kind k #> group g);
  20.106 +fun note_thmss k = gen_note_thmss (Thm.kind k);
  20.107 +fun note_thmss_grouped k g = gen_note_thmss (Thm.kind k #> Thm.group g);
  20.108  
  20.109  end;
  20.110  
  20.111 @@ -414,4 +351,3 @@
  20.112    #> Theory.add_axioms_i Proofterm.equality_axms));
  20.113  
  20.114  end;
  20.115 -
    21.1 --- a/src/Tools/induct.ML	Thu Aug 14 11:55:05 2008 +0200
    21.2 +++ b/src/Tools/induct.ML	Thu Aug 14 16:52:46 2008 +0200
    21.3 @@ -573,7 +573,7 @@
    21.4        ((fn [] => NONE | ts => List.last ts) #>
    21.5          (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
    21.6          find_inductT ctxt)) [[]]
    21.7 -  |> filter_out (forall PureThy.is_internal);
    21.8 +  |> filter_out (forall Thm.is_internal);
    21.9  
   21.10  fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   21.11    | get_inductP _ _ = [];