thm/prf: separate official name vs. additional tags;
authorwenzelm
Tue Dec 05 00:30:38 2006 +0100 (2006-12-05)
changeset 21646c07b5b0e8492
parent 21645 4af699cdfe47
child 21647 fccafa917a68
thm/prf: separate official name vs. additional tags;
src/HOL/Import/xmlconv.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/rewrite_hol_proof.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Pure/Isar/element.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/proofchecker.ML
src/Pure/Proof/reconstruct.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Thy/thm_deps.ML
src/Pure/display.ML
src/Pure/drule.ML
src/Pure/meta_simplifier.ML
src/Pure/proof_general.ML
src/Pure/proofterm.ML
src/Pure/pure_thy.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Import/xmlconv.ML	Tue Dec 05 00:29:19 2006 +0100
     1.2 +++ b/src/HOL/Import/xmlconv.ML	Tue Dec 05 00:30:38 2006 +0100
     1.3 @@ -143,7 +143,7 @@
     1.4    | xml_of_proof (prf %% prf') =
     1.5        XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
     1.6    | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
     1.7 -  | xml_of_proof (PThm ((s, _), _, t, optTs)) =
     1.8 +  | xml_of_proof (PThm (s, _, t, optTs)) =
     1.9        XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
    1.10    | xml_of_proof (PAxm (s, t, optTs)) =
    1.11        XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Dec 05 00:29:19 2006 +0100
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Dec 05 00:30:38 2006 +0100
     2.3 @@ -301,7 +301,7 @@
     2.4  (*Name management for ATP linkup. The suffix here must agree with the one given
     2.5    for notE in Clasimp.addIff*)
     2.6  fun name_notE th =
     2.7 -    Thm.name_thm (Thm.name_of_thm th ^ "_iff1", th RS notE);
     2.8 +  PureThy.put_name_hint (PureThy.get_name_hint th ^ "_iff1") (th RS notE);
     2.9        
    2.10  fun add_rules simps case_thms size_thms rec_thms inject distinct
    2.11                    weak_case_congs cong_att =
     3.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Dec 05 00:29:19 2006 +0100
     3.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Dec 05 00:30:38 2006 +0100
     3.3 @@ -128,7 +128,7 @@
     3.4            REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
     3.5              REPEAT (etac allE i) THEN atac i)) 1)]);
     3.6  
     3.7 -    val ind_name = Thm.name_of_thm induction;
     3.8 +    val ind_name = Thm.get_name induction;
     3.9      val vs = map (fn i => List.nth (pnames, i)) is;
    3.10      val (thm', thy') = thy
    3.11        |> Theory.absolute_path
    3.12 @@ -196,7 +196,7 @@
    3.13              [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
    3.14               resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
    3.15  
    3.16 -    val exh_name = Thm.name_of_thm exhaustion;
    3.17 +    val exh_name = Thm.get_name exhaustion;
    3.18      val (thm', thy') = thy
    3.19        |> Theory.absolute_path
    3.20        |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
     4.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Dec 05 00:29:19 2006 +0100
     4.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Dec 05 00:30:38 2006 +0100
     4.3 @@ -59,7 +59,7 @@
     4.4      val (Const (s, _), ts) = strip_comb S;
     4.5      val params = map dest_Var ts;
     4.6      val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
     4.7 -    fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr),
     4.8 +    fun constr_of_intr intr = (Sign.base_name (Thm.get_name intr),
     4.9        map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
    4.10          filter_out (equal Extraction.nullT) (map
    4.11            (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
    4.12 @@ -189,7 +189,7 @@
    4.13            in if conclT = Extraction.nullT
    4.14              then list_abs_free (map dest_Free xs, HOLogic.unit)
    4.15              else list_abs_free (map dest_Free xs, list_comb
    4.16 -              (Free ("r" ^ Sign.base_name (Thm.name_of_thm intr),
    4.17 +              (Free ("r" ^ Sign.base_name (Thm.get_name intr),
    4.18                  map fastype_of (rev args) ---> conclT), rev args))
    4.19            end
    4.20  
    4.21 @@ -226,7 +226,7 @@
    4.22      let
    4.23        val r = foldr1 HOLogic.mk_prod rlzs;
    4.24        val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
    4.25 -      fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr);
    4.26 +      fun name_of_fn intr = "r" ^ Sign.base_name (Thm.get_name intr);
    4.27        val r' = list_abs_free (List.mapPartial (fn intr =>
    4.28          Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs,
    4.29            if length concls = 1 then r $ x else r)
    4.30 @@ -271,7 +271,7 @@
    4.31            else forall_intr_prf (Var (hd rs), AbsP ("H", SOME rprem,
    4.32              mk_prf (tl rs) prems prf));
    4.33  
    4.34 -  in (Thm.name_of_thm rule, (vs,
    4.35 +  in (Thm.get_name rule, (vs,
    4.36      if rt = Extraction.nullt then rt else
    4.37        foldr (uncurry lambda) rt vs1,
    4.38      foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP
    4.39 @@ -349,11 +349,11 @@
    4.40      val (thy3', ind_info) = thy2 |>
    4.41        OldInductivePackage.add_inductive_i false true "" false false false
    4.42          (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
    4.43 -          ((Sign.base_name (Thm.name_of_thm intr), strip_all
    4.44 +          ((Sign.base_name (Thm.get_name intr), strip_all
    4.45              (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
    4.46        Theory.absolute_path;
    4.47      val thy3 = PureThy.hide_thms false
    4.48 -      (map Thm.name_of_thm (#intrs ind_info)) thy3';
    4.49 +      (map Thm.get_name (#intrs ind_info)) thy3';
    4.50  
    4.51      (** realizer for induction rule **)
    4.52  
    4.53 @@ -379,7 +379,7 @@
    4.54               [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
    4.55                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
    4.56          val (thm', thy') = PureThy.store_thm ((space_implode "_"
    4.57 -          (Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy
    4.58 +          (Thm.get_name induct :: vs @ Ps @ ["correctness"]), thm), []) thy
    4.59        in
    4.60          Extraction.add_realizers_i
    4.61            [mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy'
    4.62 @@ -427,7 +427,7 @@
    4.63             REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
    4.64               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
    4.65          val (thm', thy') = PureThy.store_thm ((space_implode "_"
    4.66 -          (Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
    4.67 +          (Thm.get_name elim :: vs @ Ps @ ["correctness"]), thm), []) thy
    4.68        in
    4.69          Extraction.add_realizers_i
    4.70            [mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy'
     5.1 --- a/src/HOL/Tools/meson.ML	Tue Dec 05 00:29:19 2006 +0100
     5.2 +++ b/src/HOL/Tools/meson.ML	Tue Dec 05 00:30:38 2006 +0100
     5.3 @@ -390,8 +390,7 @@
     5.4  (*Use "theorem naming" to label the clauses*)
     5.5  fun name_thms label =
     5.6      let fun name1 (th, (k,ths)) =
     5.7 -	  (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
     5.8 -
     5.9 +	  (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths)
    5.10      in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
    5.11  
    5.12  (*Is the given disjunction an all-negative support clause?*)
     6.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Dec 05 00:29:19 2006 +0100
     6.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Dec 05 00:30:38 2006 +0100
     6.3 @@ -518,17 +518,17 @@
     6.4                          cls)
     6.5   );
     6.6  
     6.7 -fun pairname th = (Thm.name_of_thm th, th);
     6.8 +fun pairname th = (PureThy.get_name_hint th, th);
     6.9  
    6.10  (*Principally for debugging*)
    6.11  fun cnf_name s = 
    6.12    let val th = thm s
    6.13 -  in cnf_axiom (Thm.name_of_thm th, th) end;
    6.14 +  in cnf_axiom (PureThy.get_name_hint th, th) end;
    6.15  
    6.16  (**** Extract and Clausify theorems from a theory's claset and simpset ****)
    6.17  
    6.18  (*Preserve the name of "th" after the transformation "f"*)
    6.19 -fun preserve_name f th = Thm.name_thm (Thm.name_of_thm th, f th);
    6.20 +fun preserve_name f th = PureThy.put_name_hint (PureThy.get_name_hint th) (f th);
    6.21  
    6.22  fun rules_of_claset cs =
    6.23    let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
    6.24 @@ -601,7 +601,7 @@
    6.25  (*** meson proof methods ***)
    6.26  
    6.27  fun skolem_use_cache_thm th =
    6.28 -  case Symtab.lookup (!clause_cache) (Thm.name_of_thm th) of
    6.29 +  case Symtab.lookup (!clause_cache) (PureThy.get_name_hint th) of
    6.30        NONE => skolem_thm th
    6.31      | SOME (th',cls) =>
    6.32          if eq_thm(th,th') then cls else skolem_thm th;
    6.33 @@ -631,7 +631,7 @@
    6.34    | conj_rule ths = foldr1 conj2_rule ths;
    6.35  
    6.36  fun skolem_attr (Context.Theory thy, th) =
    6.37 -      let val name = Thm.name_of_thm th
    6.38 +      let val name = PureThy.get_name_hint th
    6.39            val (cls, thy') = skolem_cache_thm (name, th) thy
    6.40        in (Context.Theory thy', conj_rule cls) end
    6.41    | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th));
     7.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Tue Dec 05 00:29:19 2006 +0100
     7.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Tue Dec 05 00:30:38 2006 +0100
     7.3 @@ -286,9 +286,9 @@
     7.4  
     7.5  (** Replace congruence rules by substitution rules **)
     7.6  
     7.7 -fun strip_cong ps (PThm (("HOL.cong", _), _, _, _) % _ % _ % SOME x % SOME y %%
     7.8 +fun strip_cong ps (PThm ("HOL.cong", _, _, _) % _ % _ % SOME x % SOME y %%
     7.9        prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
    7.10 -  | strip_cong ps (PThm (("HOL.refl", _), _, _, _) % SOME f) = SOME (f, ps)
    7.11 +  | strip_cong ps (PThm ("HOL.refl", _, _, _) % SOME f) = SOME (f, ps)
    7.12    | strip_cong _ _ = NONE;
    7.13  
    7.14  val subst_prf = fst (strip_combt (#2 (#der (rep_thm subst))));
    7.15 @@ -310,15 +310,15 @@
    7.16  
    7.17  fun mk_AbsP P t = AbsP ("H", P, t);
    7.18  
    7.19 -fun elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % _ % _ %% prf1 %% prf2) =
    7.20 +fun elim_cong Ts (PThm ("HOL.iffD1", _, _, _) % _ % _ %% prf1 %% prf2) =
    7.21        Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
    7.22 -  | elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % P % _ %% prf) =
    7.23 +  | elim_cong Ts (PThm ("HOL.iffD1", _, _, _) % P % _ %% prf) =
    7.24        Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
    7.25          (strip_cong [] (incr_pboundvars 1 0 prf))
    7.26 -  | elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % _ %% prf1 %% prf2) =
    7.27 +  | elim_cong Ts (PThm ("HOL.iffD2", _, _, _) % _ % _ %% prf1 %% prf2) =
    7.28        Option.map (make_subst Ts prf2 [] o
    7.29          apsnd (map (make_sym Ts))) (strip_cong [] prf1)
    7.30 -  | elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % P %% prf) =
    7.31 +  | elim_cong Ts (PThm ("HOL.iffD2", _, _, _) % _ % P %% prf) =
    7.32        Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
    7.33          apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
    7.34    | elim_cong _ _ = NONE;
     8.1 --- a/src/Provers/clasimp.ML	Tue Dec 05 00:29:19 2006 +0100
     8.2 +++ b/src/Provers/clasimp.ML	Tue Dec 05 00:30:38 2006 +0100
     8.3 @@ -115,8 +115,8 @@
     8.4                              CHANGED o Simplifier.asm_lr_simp_tac ss));
     8.5  
     8.6  (*Attach a suffix, provided we have a name to start with.*)
     8.7 -fun suffix_thm "" _ th = th
     8.8 -  | suffix_thm a b th = Thm.name_thm (a^b, th);
     8.9 +fun suffix_thm "" _ = I
    8.10 +  | suffix_thm a b = PureThy.put_name_hint (a^b);
    8.11  
    8.12  (* iffs: addition of rules to simpsets and clasets simultaneously *)
    8.13  
    8.14 @@ -129,7 +129,7 @@
    8.15  
    8.16  fun addIff decls1 decls2 simp ((cs, ss), th) =
    8.17    let
    8.18 -    val name = Thm.name_of_thm th;
    8.19 +    val name = PureThy.get_name_hint th;
    8.20      val n = nprems_of th;
    8.21      val (elim, intro) = if n = 0 then decls1 else decls2;
    8.22      val zero_rotate = zero_var_indexes o rotate_prems n;
     9.1 --- a/src/Provers/classical.ML	Tue Dec 05 00:29:19 2006 +0100
     9.2 +++ b/src/Provers/classical.ML	Tue Dec 05 00:30:38 2006 +0100
     9.3 @@ -195,7 +195,7 @@
     9.4            else all_tac))
     9.5          |> Seq.hd
     9.6          |> Drule.zero_var_indexes
     9.7 -        |> Thm.put_name_tags (Thm.get_name_tags rule);
     9.8 +        |> PureThy.put_name_hint (PureThy.get_name_hint rule);
     9.9      in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
    9.10    else rule;
    9.11  
    9.12 @@ -424,9 +424,9 @@
    9.13      if has_fewer_prems 1 th then
    9.14      	error("Ill-formed destruction rule\n" ^ string_of_thm th)
    9.15      else
    9.16 -    case Thm.name_of_thm th of
    9.17 +    case PureThy.get_name_hint th of
    9.18          "" => Tactic.make_elim th
    9.19 -      | a  => Thm.name_thm (a ^ "_dest", Tactic.make_elim th);
    9.20 +      | a  => PureThy.put_name_hint (a ^ "_dest") (Tactic.make_elim th);
    9.21  
    9.22  fun cs addSDs ths = cs addSEs (map name_make_elim ths);
    9.23  
    10.1 --- a/src/Pure/Isar/element.ML	Tue Dec 05 00:29:19 2006 +0100
    10.2 +++ b/src/Pure/Isar/element.ML	Tue Dec 05 00:30:38 2006 +0100
    10.3 @@ -226,7 +226,7 @@
    10.4  
    10.5  fun thm_name kind th prts =
    10.6    let val head =
    10.7 -    (case #1 (Thm.get_name_tags th) of
    10.8 +    (case PureThy.get_name_hint th of
    10.9        "" => Pretty.command kind
   10.10      | a => Pretty.block [Pretty.command kind, Pretty.brk 1, Pretty.str (Sign.base_name a ^ ":")])
   10.11    in Pretty.block (Pretty.fbreaks (head :: prts)) end;
    11.1 --- a/src/Pure/Isar/rule_cases.ML	Tue Dec 05 00:29:19 2006 +0100
    11.2 +++ b/src/Pure/Isar/rule_cases.ML	Tue Dec 05 00:30:38 2006 +0100
    11.3 @@ -215,7 +215,7 @@
    11.4  
    11.5  fun lookup_consumes th =
    11.6    let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [th]) in
    11.7 -    (case AList.lookup (op =) (Thm.tags_of_thm th) (consumes_tagN) of
    11.8 +    (case AList.lookup (op =) (Thm.get_tags th) (consumes_tagN) of
    11.9        NONE => NONE
   11.10      | SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ())
   11.11      | _ => err ())
   11.12 @@ -249,7 +249,7 @@
   11.13        PureThy.untag_rule case_names_tagN
   11.14        #> PureThy.tag_rule (case_names_tagN, names);
   11.15  
   11.16 -fun lookup_case_names th = AList.lookup (op =) (Thm.tags_of_thm th) case_names_tagN;
   11.17 +fun lookup_case_names th = AList.lookup (op =) (Thm.get_tags th) case_names_tagN;
   11.18  
   11.19  val save_case_names = add_case_names o lookup_case_names;
   11.20  val name = add_case_names o SOME;
   11.21 @@ -264,16 +264,16 @@
   11.22  fun is_case_concl name ((a, b :: _): tag) = (a = case_concl_tagN andalso b = name)
   11.23    | is_case_concl _ _ = false;
   11.24  
   11.25 -fun add_case_concl (name, cs) = PureThy.map_tags (fn tags =>
   11.26 +fun add_case_concl (name, cs) = Thm.map_tags (fn tags =>
   11.27    filter_out (is_case_concl name) tags @ [(case_concl_tagN, name :: cs)]);
   11.28  
   11.29  fun get_case_concls th name =
   11.30 -  (case find_first (is_case_concl name) (Thm.tags_of_thm th) of
   11.31 +  (case find_first (is_case_concl name) (Thm.get_tags th) of
   11.32      SOME (_, _ :: cs) => cs
   11.33    | _ => []);
   11.34  
   11.35  fun save_case_concls th =
   11.36 -  let val concls = Thm.tags_of_thm th |> map_filter
   11.37 +  let val concls = Thm.get_tags th |> map_filter
   11.38      (fn (a, b :: cs) =>
   11.39        if a = case_concl_tagN then SOME (b, cs) else NONE
   11.40      | _ => NONE)
    12.1 --- a/src/Pure/Proof/extraction.ML	Tue Dec 05 00:29:19 2006 +0100
    12.2 +++ b/src/Pure/Proof/extraction.ML	Tue Dec 05 00:30:38 2006 +0100
    12.3 @@ -314,7 +314,7 @@
    12.4      val rd = ProofSyntax.read_proof thy' false
    12.5    in fn (thm, (vs, s1, s2)) =>
    12.6      let
    12.7 -      val name = Thm.name_of_thm thm;
    12.8 +      val name = Thm.get_name thm;
    12.9        val _ = assert (name <> "") "add_realizers: unnamed theorem";
   12.10        val prop = Pattern.rewrite_term thy'
   12.11          (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
   12.12 @@ -359,7 +359,7 @@
   12.13      val {realizes_eqns, typeof_eqns, types, realizers,
   12.14        defs, expand, prep} = ExtractionData.get thy;
   12.15  
   12.16 -    val name = Thm.name_of_thm thm;
   12.17 +    val name = Thm.get_name thm;
   12.18      val _ = assert (name <> "") "add_expand_thms: unnamed theorem";
   12.19  
   12.20      val is_def =
   12.21 @@ -555,7 +555,7 @@
   12.22                (defs3, corr_prf1 % u %% corr_prf2)
   12.23            end
   12.24  
   12.25 -      | corr d defs vs ts Ts hs (prf0 as PThm ((name, _), prf, prop, SOME Ts')) _ _ =
   12.26 +      | corr d defs vs ts Ts hs (prf0 as PThm (name, prf, prop, SOME Ts')) _ _ =
   12.27            let
   12.28              val (vs', tye) = find_inst prop Ts ts vs;
   12.29              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye;
   12.30 @@ -578,7 +578,7 @@
   12.31                      val corr_prop = Reconstruct.prop_of corr_prf;
   12.32                      val corr_prf' = foldr forall_intr_prf
   12.33                        (proof_combt
   12.34 -                         (PThm ((corr_name name vs', []), corr_prf, corr_prop,
   12.35 +                         (PThm (corr_name name vs', corr_prf, corr_prop,
   12.36                               SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
   12.37  		      (map (get_var_type corr_prop) (vfs_of prop))
   12.38                    in
   12.39 @@ -643,7 +643,7 @@
   12.40                in (defs'', f $ t) end
   12.41            end
   12.42  
   12.43 -      | extr d defs vs ts Ts hs (prf0 as PThm ((s, _), prf, prop, SOME Ts')) =
   12.44 +      | extr d defs vs ts Ts hs (prf0 as PThm (s, prf, prop, SOME Ts')) =
   12.45            let
   12.46              val (vs', tye) = find_inst prop Ts ts vs;
   12.47              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
   12.48 @@ -687,7 +687,7 @@
   12.49                      val corr_prop = Reconstruct.prop_of corr_prf';
   12.50                      val corr_prf'' = foldr forall_intr_prf
   12.51                        (proof_combt
   12.52 -                        (PThm ((corr_name s vs', []), corr_prf', corr_prop,
   12.53 +                        (PThm (corr_name s vs', corr_prf', corr_prop,
   12.54                            SOME (map TVar (term_tvars corr_prop))),  vfs_of corr_prop))
   12.55  		      (map (get_var_type corr_prop) (vfs_of prop));
   12.56                    in
   12.57 @@ -719,7 +719,7 @@
   12.58      fun prep_thm (thm, vs) =
   12.59        let
   12.60          val {prop, der = (_, prf), sign, ...} = rep_thm thm;
   12.61 -        val name = Thm.name_of_thm thm;
   12.62 +        val name = Thm.get_name thm;
   12.63          val _ = assert (name <> "") "extraction: unnamed theorem";
   12.64          val _ = assert (etype_of thy' vs [] prop <> nullT) ("theorem " ^
   12.65            quote name ^ " has no computational content")
    13.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Dec 05 00:29:19 2006 +0100
    13.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Dec 05 00:30:38 2006 +0100
    13.3 @@ -32,12 +32,12 @@
    13.4      val equal_elim_axm = ax equal_elim_axm [];
    13.5      val symmetric_axm = ax symmetric_axm [propT];
    13.6  
    13.7 -    fun rew' (PThm (("ProtoPure.protectD", _), _, _, _) % _ %%
    13.8 -        (PThm (("ProtoPure.protectI", _), _, _, _) % _ %% prf)) = SOME prf
    13.9 -      | rew' (PThm (("ProtoPure.conjunctionD1", _), _, _, _) % _ % _ %%
   13.10 -        (PThm (("ProtoPure.conjunctionI", _), _, _, _) % _ % _ %% prf %% _)) = SOME prf
   13.11 -      | rew' (PThm (("ProtoPure.conjunctionD2", _), _, _, _) % _ % _ %%
   13.12 -        (PThm (("ProtoPure.conjunctionI", _), _, _, _) % _ % _ %% _ %% prf)) = SOME prf
   13.13 +    fun rew' (PThm ("ProtoPure.protectD", _, _, _) % _ %%
   13.14 +        (PThm ("ProtoPure.protectI", _, _, _) % _ %% prf)) = SOME prf
   13.15 +      | rew' (PThm ("ProtoPure.conjunctionD1", _, _, _) % _ % _ %%
   13.16 +        (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% prf %% _)) = SOME prf
   13.17 +      | rew' (PThm ("ProtoPure.conjunctionD2", _, _, _) % _ % _ %%
   13.18 +        (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% _ %% prf)) = SOME prf
   13.19        | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   13.20          (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
   13.21        | rew' (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   13.22 @@ -47,14 +47,14 @@
   13.23        | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
   13.24          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
   13.25            _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
   13.26 -        ((tg as PThm (("ProtoPure.protectI", _), _, _, _)) % _ %% prf2)) =
   13.27 +        ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) =
   13.28          SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
   13.29  
   13.30        | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
   13.31          (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   13.32            (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
   13.33               _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
   13.34 -        ((tg as PThm (("ProtoPure.protectI", _), _, _, _)) % _ %% prf2)) =
   13.35 +        ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) =
   13.36          SOME (tg %> B %% (equal_elim_axm %> A %> B %%
   13.37            (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
   13.38  
   13.39 @@ -222,7 +222,7 @@
   13.40    | insert_refl defs Ts (AbsP (s, t, prf)) =
   13.41        AbsP (s, t, insert_refl defs Ts prf)
   13.42    | insert_refl defs Ts prf = (case strip_combt prf of
   13.43 -        (PThm ((s, _), _, prop, SOME Ts), ts) =>
   13.44 +        (PThm (s, _, prop, SOME Ts), ts) =>
   13.45            if member (op =) defs s then
   13.46              let
   13.47                val vs = vars_of prop;
   13.48 @@ -241,7 +241,7 @@
   13.49  fun elim_defs thy r defs prf =
   13.50    let
   13.51      val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
   13.52 -    val defnames = map Thm.name_of_thm defs;
   13.53 +    val defnames = map Thm.get_name defs;
   13.54      val f = if not r then I else
   13.55        let
   13.56          val cnames = map (fst o dest_Const o fst) defs';
    14.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Dec 05 00:29:19 2006 +0100
    14.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Dec 05 00:30:38 2006 +0100
    14.3 @@ -108,12 +108,12 @@
    14.4        | rename (AbsP (s, t, prf)) = AbsP (s, t, rename prf)
    14.5        | rename (prf1 %% prf2) = rename prf1 %% rename prf2
    14.6        | rename (prf % t) = rename prf % t
    14.7 -      | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
    14.8 +      | rename (prf' as PThm (s, prf, prop, Ts)) =
    14.9            let
   14.10              val prop' = the_default (Bound 0) (AList.lookup (op =) thms' s);
   14.11              val ps = remove (op =) prop' (map fst (the (Symtab.lookup thms s)))
   14.12            in if prop = prop' then prf' else
   14.13 -            PThm ((s ^ "_" ^ string_of_int (length ps - find_index (fn p => p = prop) ps), tags),
   14.14 +            PThm (s ^ "_" ^ string_of_int (length ps - find_index (fn p => p = prop) ps),
   14.15                prf, prop, Ts)
   14.16            end
   14.17        | rename prf = prf
   14.18 @@ -183,9 +183,9 @@
   14.19  val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
   14.20    [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
   14.21  
   14.22 -fun term_of _ (PThm ((name, _), _, _, NONE)) =
   14.23 +fun term_of _ (PThm (name, _, _, NONE)) =
   14.24        Const (NameSpace.append "thm" name, proofT)
   14.25 -  | term_of _ (PThm ((name, _), _, _, SOME Ts)) =
   14.26 +  | term_of _ (PThm (name, _, _, SOME Ts)) =
   14.27        mk_tyapp Ts (Const (NameSpace.append "thm" name, proofT))
   14.28    | term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT)
   14.29    | term_of _ (PAxm (name, _, SOME Ts)) =
    15.1 --- a/src/Pure/Proof/proofchecker.ML	Tue Dec 05 00:29:19 2006 +0100
    15.2 +++ b/src/Pure/Proof/proofchecker.ML	Tue Dec 05 00:30:38 2006 +0100
    15.3 @@ -45,7 +45,7 @@
    15.4          Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm'))
    15.5        end;
    15.6  
    15.7 -    fun thm_of _ _ (PThm ((name, _), _, prop', SOME Ts)) =
    15.8 +    fun thm_of _ _ (PThm (name, _, prop', SOME Ts)) =
    15.9            let
   15.10              val thm = Drule.implies_intr_hyps (lookup name);
   15.11              val {prop, ...} = rep_thm thm;
    16.1 --- a/src/Pure/Proof/reconstruct.ML	Tue Dec 05 00:29:19 2006 +0100
    16.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Dec 05 00:30:38 2006 +0100
    16.3 @@ -151,7 +151,7 @@
    16.4              val prop'' = subst_TVars (map fst tvars @ map snd fmap ~~ Ts)
    16.5                (forall_intr_vfs prop') handle Library.UnequalLengths =>
    16.6                  error ("Wrong number of type arguments for " ^
    16.7 -                  quote (fst (get_name_tags [] prop prf)))
    16.8 +                  quote (get_name [] prop prf))
    16.9            in (prop'', change_type (SOME Ts) prf, [], env', vTs) end;
   16.10  
   16.11      fun head_norm (prop, prf, cnstrts, env, vTs) =
   16.12 @@ -352,7 +352,7 @@
   16.13        | expand maxidx prfs (prf % t) =
   16.14            let val (maxidx', prfs', prf') = expand maxidx prfs prf
   16.15            in (maxidx', prfs', prf' % t) end
   16.16 -      | expand maxidx prfs (prf as PThm ((a, _), cprf, prop, SOME Ts)) =
   16.17 +      | expand maxidx prfs (prf as PThm (a, cprf, prop, SOME Ts)) =
   16.18            if not (exists
   16.19              (fn (b, NONE) => a = b
   16.20                | (b, SOME prop') => a = b andalso prop = prop') thms)
    17.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Dec 05 00:29:19 2006 +0100
    17.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Dec 05 00:30:38 2006 +0100
    17.3 @@ -338,7 +338,7 @@
    17.4  (* FIXME: check this uses non-transitive closure function here *)
    17.5  fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
    17.6    let
    17.7 -    val names = filter_out (equal "") (map Thm.name_of_thm ths);
    17.8 +    val names = filter_out (equal "") (map PureThy.get_name_hint ths);
    17.9      val deps = filter_out (equal "")
   17.10        (Symtab.keys (fold Proofterm.thms_of_proof
   17.11          (map Thm.proof_of ths) Symtab.empty));
    18.1 --- a/src/Pure/Thy/thm_deps.ML	Tue Dec 05 00:29:19 2006 +0100
    18.2 +++ b/src/Pure/Thy/thm_deps.ML	Tue Dec 05 00:30:38 2006 +0100
    18.3 @@ -25,9 +25,9 @@
    18.4  fun enable () = if ! proofs = 0 then proofs := 1 else ();
    18.5  fun disable () = proofs := 0;
    18.6  
    18.7 -fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
    18.8 -  | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof ([], [], []))
    18.9 -  | dest_thm_axm _ = (("", []), MinProof ([], [], []));
   18.10 +fun dest_thm_axm (PThm (name, prf, _, _)) = (name, prf)
   18.11 +  | dest_thm_axm (PAxm (name, _, _)) = (name ^ " (Ax)", MinProof ([], [], []))
   18.12 +  | dest_thm_axm _ = ("", MinProof ([], [], []));
   18.13  
   18.14  fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf
   18.15    | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf
   18.16 @@ -37,9 +37,9 @@
   18.17        fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #>
   18.18        fold (make_deps_graph o Proofterm.proof_of_min_axm) axms
   18.19    | make_deps_graph prf = (fn p as (gra, parents) =>
   18.20 -      let val ((name, tags), prf') = dest_thm_axm prf
   18.21 +      let val (name, prf') = dest_thm_axm prf
   18.22        in
   18.23 -        if name <> "" andalso not (PureThy.has_internal tags) then
   18.24 +        if name <> "" then
   18.25            if not (Symtab.defined gra name) then
   18.26              let
   18.27                val (gra', parents') = make_deps_graph prf' (gra, []);
    19.1 --- a/src/Pure/display.ML	Tue Dec 05 00:29:19 2006 +0100
    19.2 +++ b/src/Pure/display.ML	Tue Dec 05 00:30:38 2006 +0100
    19.3 @@ -77,7 +77,7 @@
    19.4      val th = Thm.strip_shyps raw_th;
    19.5      val {hyps, tpairs, prop, der = (ora, _), ...} = Thm.rep_thm th;
    19.6      val xshyps = Thm.extra_shyps th;
    19.7 -    val (_, tags) = Thm.get_name_tags th;
    19.8 +    val tags = Thm.get_tags th;
    19.9  
   19.10      val q = if quote then Pretty.quote else I;
   19.11      val prt_term = q o (Pretty.term pp);
    20.1 --- a/src/Pure/drule.ML	Tue Dec 05 00:29:19 2006 +0100
    20.2 +++ b/src/Pure/drule.ML	Tue Dec 05 00:30:38 2006 +0100
    20.3 @@ -427,7 +427,7 @@
    20.4      |      _   => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
    20.5  
    20.6  fun close_derivation thm =
    20.7 -  if Thm.get_name_tags thm = ("", []) then Thm.name_thm ("", thm)
    20.8 +  if Thm.get_name thm = "" then Thm.put_name "" thm
    20.9    else thm;
   20.10  
   20.11  
    21.1 --- a/src/Pure/meta_simplifier.ML	Tue Dec 05 00:29:19 2006 +0100
    21.2 +++ b/src/Pure/meta_simplifier.ML	Tue Dec 05 00:30:38 2006 +0100
    21.3 @@ -514,7 +514,7 @@
    21.4    end;
    21.5  
    21.6  fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
    21.7 -  maps (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms;
    21.8 +  maps (fn thm => map (rpair (PureThy.get_name_hint thm)) (mk thm)) thms;
    21.9  
   21.10  fun extract_safe_rrules (ss, thm) =
   21.11    maps (orient_rrule ss) (extract_rews (ss, [thm]));
    22.1 --- a/src/Pure/proof_general.ML	Tue Dec 05 00:29:19 2006 +0100
    22.2 +++ b/src/Pure/proof_general.ML	Tue Dec 05 00:30:38 2006 +0100
    22.3 @@ -481,7 +481,7 @@
    22.4  (* FIXME: check this uses non-transitive closure function here *)
    22.5  fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
    22.6    let
    22.7 -    val names = filter_out (equal "") (map Thm.name_of_thm ths);
    22.8 +    val names = filter_out (equal "") (map PureThy.get_name_hint ths);
    22.9      val deps = filter_out (equal "")
   22.10        (Symtab.keys (fold Proofterm.thms_of_proof
   22.11          (map Thm.proof_of ths) Symtab.empty));
    23.1 --- a/src/Pure/proofterm.ML	Tue Dec 05 00:29:19 2006 +0100
    23.2 +++ b/src/Pure/proofterm.ML	Tue Dec 05 00:30:38 2006 +0100
    23.3 @@ -18,7 +18,7 @@
    23.4     | % of proof * term option
    23.5     | %% of proof * proof
    23.6     | Hyp of term
    23.7 -   | PThm of (string * (string * string list) list) * proof * term * typ list option
    23.8 +   | PThm of string * proof * term * typ list option
    23.9     | PAxm of string * term * typ list option
   23.10     | Oracle of string * term * typ list option
   23.11     | MinProof of ((string * term) * proof) list * (string * term) list * (string * term) list;
   23.12 @@ -99,9 +99,8 @@
   23.13    val equal_elim : term -> term -> proof -> proof -> proof
   23.14    val axm_proof : string -> term -> proof
   23.15    val oracle_proof : string -> term -> proof
   23.16 -  val thm_proof : theory -> string * (string * string list) list ->
   23.17 -    term list -> term -> proof -> proof
   23.18 -  val get_name_tags : term list -> term -> proof -> string * (string * string list) list
   23.19 +  val thm_proof : theory -> string -> term list -> term -> proof -> proof
   23.20 +  val get_name : term list -> term -> proof -> string
   23.21  
   23.22    (** rewriting on proof terms **)
   23.23    val add_prf_rrules : (proof * proof) list -> theory -> theory
   23.24 @@ -112,7 +111,7 @@
   23.25    val rewrite_proof_notypes : (proof * proof) list *
   23.26      (string * (typ list -> proof -> proof option)) list -> proof -> proof
   23.27    val init_data: theory -> theory
   23.28 -  
   23.29 +
   23.30  end
   23.31  
   23.32  structure Proofterm : PROOFTERM =
   23.33 @@ -127,13 +126,13 @@
   23.34   | op % of proof * term option
   23.35   | op %% of proof * proof
   23.36   | Hyp of term
   23.37 - | PThm of (string * (string * string list) list) * proof * term * typ list option
   23.38 + | PThm of string * proof * term * typ list option
   23.39   | PAxm of string * term * typ list option
   23.40   | Oracle of string * term * typ list option
   23.41   | MinProof of ((string * term) * proof) list * (string * term) list * (string * term) list;
   23.42  
   23.43  fun proof_of_min_axm (s, prop) = PAxm (s, prop, NONE);
   23.44 -fun proof_of_min_thm ((s, prop), prf) = PThm ((s, []), prf, prop, NONE);
   23.45 +fun proof_of_min_thm ((s, prop), prf) = PThm (s, prf, prop, NONE);
   23.46  
   23.47  val string_term_ord = prod_ord fast_string_ord Term.fast_term_ord;
   23.48  
   23.49 @@ -143,7 +142,7 @@
   23.50        | oras_of (AbsP (_, _, prf)) = oras_of prf
   23.51        | oras_of (prf % _) = oras_of prf
   23.52        | oras_of (prf1 %% prf2) = oras_of prf1 #> oras_of prf2
   23.53 -      | oras_of (PThm ((name, _), prf, prop, _)) = (fn tabs as (thms, oras) =>
   23.54 +      | oras_of (PThm (name, prf, prop, _)) = (fn tabs as (thms, oras) =>
   23.55            case Symtab.lookup thms name of
   23.56              NONE => oras_of prf (Symtab.update (name, [prop]) thms, oras)
   23.57            | SOME ps => if member (op =) ps prop then tabs else
   23.58 @@ -162,7 +161,7 @@
   23.59    | thms_of_proof (AbsP (_, _, prf)) = thms_of_proof prf
   23.60    | thms_of_proof (prf1 %% prf2) = thms_of_proof prf1 #> thms_of_proof prf2
   23.61    | thms_of_proof (prf % _) = thms_of_proof prf
   23.62 -  | thms_of_proof (prf' as PThm ((s, _), prf, prop, _)) = (fn tab =>
   23.63 +  | thms_of_proof (prf' as PThm (s, prf, prop, _)) = (fn tab =>
   23.64        case Symtab.lookup tab s of
   23.65          NONE => thms_of_proof prf (Symtab.update (s, [(prop, prf')]) tab)
   23.66        | SOME ps => if exists (fn (p, _) => p = prop) ps then tab else
   23.67 @@ -175,8 +174,8 @@
   23.68    | thms_of_proof' (AbsP (_, _, prf)) = thms_of_proof' prf
   23.69    | thms_of_proof' (prf1 %% prf2) = thms_of_proof' prf1 #> thms_of_proof' prf2
   23.70    | thms_of_proof' (prf % _) = thms_of_proof' prf
   23.71 -  | thms_of_proof' (PThm (("", _), prf, prop, _)) = thms_of_proof' prf
   23.72 -  | thms_of_proof' (prf' as PThm ((s, _), _, prop, _)) = (fn tab =>
   23.73 +  | thms_of_proof' (PThm ("", prf, prop, _)) = thms_of_proof' prf
   23.74 +  | thms_of_proof' (prf' as PThm (s, _, prop, _)) = (fn tab =>
   23.75        case Symtab.lookup tab s of
   23.76          NONE => Symtab.update (s, [(prop, prf')]) tab
   23.77        | SOME ps => if exists (fn (p, _) => p = prop) ps then tab else
   23.78 @@ -200,7 +199,7 @@
   23.79    | mk_min_proof (AbsP (_, _, prf)) = mk_min_proof prf
   23.80    | mk_min_proof (prf % _) = mk_min_proof prf
   23.81    | mk_min_proof (prf1 %% prf2) = mk_min_proof prf1 #> mk_min_proof prf2
   23.82 -  | mk_min_proof (PThm ((s, _), prf, prop, _)) =
   23.83 +  | mk_min_proof (PThm (s, prf, prop, _)) =
   23.84        map3 (OrdList.insert (string_term_ord o pairself fst) ((s, prop), prf)) I I
   23.85    | mk_min_proof (PAxm (s, prop, _)) =
   23.86        map3 I (OrdList.insert string_term_ord (s, prop)) I
   23.87 @@ -239,12 +238,12 @@
   23.88  val proof_combt' = Library.foldl (op %);
   23.89  val proof_combP = Library.foldl (op %%);
   23.90  
   23.91 -fun strip_combt prf = 
   23.92 +fun strip_combt prf =
   23.93      let fun stripc (prf % t, ts) = stripc (prf, t::ts)
   23.94 -          | stripc  x =  x 
   23.95 +          | stripc  x =  x
   23.96      in  stripc (prf, [])  end;
   23.97  
   23.98 -fun strip_combP prf = 
   23.99 +fun strip_combP prf =
  23.100      let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs)
  23.101            | stripc  x =  x
  23.102      in  stripc (prf, [])  end;
  23.103 @@ -330,7 +329,7 @@
  23.104  fun mk_abs Ts t = Library.foldl (fn (t', T) => Abs ("", T, t')) (t, Ts);
  23.105  
  23.106  
  23.107 -(*Abstraction of a proof term over its occurrences of v, 
  23.108 +(*Abstraction of a proof term over its occurrences of v,
  23.109      which must contain no loose bound variables.
  23.110    The resulting proof term is ready to become the body of an Abst.*)
  23.111  
  23.112 @@ -365,17 +364,17 @@
  23.113  fun incr_bv' inct tlev t = incr_bv (inct, tlev, t);
  23.114  
  23.115  fun prf_incr_bv' incP inct Plev tlev (PBound i) =
  23.116 -      if i >= Plev then PBound (i+incP) else raise SAME 
  23.117 +      if i >= Plev then PBound (i+incP) else raise SAME
  23.118    | prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) =
  23.119        (AbsP (a, apsome' (same (incr_bv' inct tlev)) t,
  23.120           prf_incr_bv incP inct (Plev+1) tlev body) handle SAME =>
  23.121             AbsP (a, t, prf_incr_bv' incP inct (Plev+1) tlev body))
  23.122    | prf_incr_bv' incP inct Plev tlev (Abst (a, T, body)) =
  23.123        Abst (a, T, prf_incr_bv' incP inct Plev (tlev+1) body)
  23.124 -  | prf_incr_bv' incP inct Plev tlev (prf %% prf') = 
  23.125 +  | prf_incr_bv' incP inct Plev tlev (prf %% prf') =
  23.126        (prf_incr_bv' incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf'
  23.127         handle SAME => prf %% prf_incr_bv' incP inct Plev tlev prf')
  23.128 -  | prf_incr_bv' incP inct Plev tlev (prf % t) = 
  23.129 +  | prf_incr_bv' incP inct Plev tlev (prf % t) =
  23.130        (prf_incr_bv' incP inct Plev tlev prf % Option.map (incr_bv' inct tlev) t
  23.131         handle SAME => prf % apsome' (same (incr_bv' inct tlev)) t)
  23.132    | prf_incr_bv' _ _ _ _ _ = raise SAME
  23.133 @@ -539,7 +538,7 @@
  23.134    | thaw names names' (Abs (s, T, t)) =
  23.135        Abs (s, thawT names' T, thaw names names' t)
  23.136    | thaw names names' (Const (s, T)) = Const (s, thawT names' T)
  23.137 -  | thaw names names' (Free (s, T)) = 
  23.138 +  | thaw names names' (Free (s, T)) =
  23.139        let val T' = thawT names' T
  23.140        in case AList.lookup (op =) names s of
  23.141            NONE => Free (s, T')
  23.142 @@ -703,12 +702,12 @@
  23.143      val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop);
  23.144      val k = length ps;
  23.145  
  23.146 -    fun mk_app (b, (i, j, prf)) = 
  23.147 +    fun mk_app (b, (i, j, prf)) =
  23.148            if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
  23.149  
  23.150      fun lift Us bs i j (Const ("==>", _) $ A $ B) =
  23.151              AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B)
  23.152 -      | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) = 
  23.153 +      | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) =
  23.154              Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
  23.155        | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
  23.156              map (fn k => (#3 (foldr mk_app (i-1, j-1, PBound k) bs)))
  23.157 @@ -888,7 +887,7 @@
  23.158        | t' => is_p 0 t')
  23.159    end;
  23.160  
  23.161 -fun needed_vars prop = 
  23.162 +fun needed_vars prop =
  23.163    Library.foldl (op union)
  23.164      ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))) union
  23.165    prop_vars prop;
  23.166 @@ -915,7 +914,7 @@
  23.167    let
  23.168      val compress_typ = Compress.typ thy;
  23.169      val compress_term = Compress.term thy;
  23.170 -  
  23.171 +
  23.172      fun shrink ls lev (prf as Abst (a, T, body)) =
  23.173            let val (b, is, ch, body') = shrink ls (lev+1) body
  23.174            in (b, is, ch, if ch then Abst (a, Option.map compress_typ T, body') else prf) end
  23.175 @@ -1029,8 +1028,7 @@
  23.176            mtch Ts (i+1) j (optmatch (matcht Ts j) inst (opt, opu)) (prf1, prf2)
  23.177        | mtch Ts i j inst (prf1, AbsP (_, _, prf2)) =
  23.178            mtch Ts (i+1) j inst (incr_pboundvars 1 0 prf1 %% PBound 0, prf2)
  23.179 -      | mtch Ts i j inst (PThm ((name1, _), _, prop1, opTs),
  23.180 -            PThm ((name2, _), _, prop2, opUs)) =
  23.181 +      | mtch Ts i j inst (PThm (name1, _, prop1, opTs), PThm (name2, _, prop2, opUs)) =
  23.182            if name1=name2 andalso prop1=prop2 then
  23.183              optmatch matchTs inst (opTs, opUs)
  23.184            else raise PMatch
  23.185 @@ -1070,7 +1068,7 @@
  23.186        | subst _ _ t = t
  23.187    in subst 0 0 end;
  23.188  
  23.189 -(*A fast unification filter: true unless the two terms cannot be unified. 
  23.190 +(*A fast unification filter: true unless the two terms cannot be unified.
  23.191    Terms must be NORMAL.  Treats all Vars as distinct. *)
  23.192  fun could_unify prf1 prf2 =
  23.193    let
  23.194 @@ -1088,7 +1086,7 @@
  23.195    in case (head_of prf1, head_of prf2) of
  23.196          (_, Hyp (Var _)) => true
  23.197        | (Hyp (Var _), _) => true
  23.198 -      | (PThm ((a, _), _, propa, _), PThm ((b, _), _, propb, _)) =>
  23.199 +      | (PThm (a, _, propa, _), PThm (b, _, propb, _)) =>
  23.200            a = b andalso propa = propb andalso matchrands prf1 prf2
  23.201        | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
  23.202        | (PBound i, PBound j) =>  i = j andalso matchrands prf1 prf2
  23.203 @@ -1203,7 +1201,7 @@
  23.204    let val r = ProofData.get thy
  23.205    in ProofData.put (fst r, ps @ snd r) thy end;
  23.206  
  23.207 -fun thm_proof thy (name, tags) hyps prop prf =
  23.208 +fun thm_proof thy name hyps prop prf =
  23.209    let
  23.210      val prop = Logic.list_implies (hyps, prop);
  23.211      val nvs = needed_vars prop;
  23.212 @@ -1215,25 +1213,23 @@
  23.213            (foldr (uncurry implies_intr_proof) prf hyps)))
  23.214        else MinProof (mk_min_proof prf ([], [], []));
  23.215      val head = (case strip_combt (fst (strip_combP prf)) of
  23.216 -        (PThm ((old_name, _), prf', prop', NONE), args') =>
  23.217 +        (PThm (old_name, prf', prop', NONE), args') =>
  23.218            if (old_name="" orelse old_name=name) andalso
  23.219               prop = prop' andalso args = args' then
  23.220 -            PThm ((name, tags), prf', prop, NONE)
  23.221 +            PThm (name, prf', prop, NONE)
  23.222            else
  23.223 -            PThm ((name, tags), opt_prf, prop, NONE)
  23.224 -      | _ => PThm ((name, tags), opt_prf, prop, NONE))
  23.225 +            PThm (name, opt_prf, prop, NONE)
  23.226 +      | _ => PThm (name, opt_prf, prop, NONE))
  23.227    in
  23.228      proof_combP (proof_combt' (head, args), map Hyp hyps)
  23.229    end;
  23.230  
  23.231 -fun get_name_tags hyps prop prf =
  23.232 +fun get_name hyps prop prf =
  23.233    let val prop = Logic.list_implies (hyps, prop) in
  23.234      (case strip_combt (fst (strip_combP prf)) of
  23.235 -      (PThm ((name, tags), _, prop', _), _) =>
  23.236 -        if prop=prop' then (name, tags) else ("", [])
  23.237 -    | (PAxm (name, prop', _), _) =>
  23.238 -        if prop=prop' then (name, []) else ("", [])
  23.239 -    | _ => ("", []))
  23.240 +      (PThm (name, _, prop', _), _) => if prop=prop' then name else ""
  23.241 +    | (PAxm (name, prop', _), _) => if prop=prop' then name else ""
  23.242 +    | _ => "")
  23.243    end;
  23.244  
  23.245  end;
    24.1 --- a/src/Pure/pure_thy.ML	Tue Dec 05 00:29:19 2006 +0100
    24.2 +++ b/src/Pure/pure_thy.ML	Tue Dec 05 00:30:38 2006 +0100
    24.3 @@ -29,11 +29,12 @@
    24.4  signature PURE_THY =
    24.5  sig
    24.6    include BASIC_PURE_THY
    24.7 -  val map_tags: (tag list -> tag list) -> thm -> thm
    24.8    val tag_rule: tag -> thm -> thm
    24.9    val untag_rule: string -> thm -> thm
   24.10    val tag: tag -> attribute
   24.11    val untag: string -> attribute
   24.12 +  val get_name_hint: thm -> string
   24.13 +  val put_name_hint: string -> thm -> thm
   24.14    val get_kind: thm -> string
   24.15    val kind_rule: string -> thm -> thm
   24.16    val kind: string -> attribute
   24.17 @@ -62,7 +63,9 @@
   24.18    val burrow_facts: ('a list -> 'b list) ->
   24.19      ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
   24.20    val name_multi: string -> 'a list -> (string * 'a) list
   24.21 -  val name_thm: bool -> string * thm -> thm
   24.22 +  val name_thm: bool -> bool -> string -> thm -> thm
   24.23 +  val name_thms: bool -> bool -> string -> thm list -> thm list
   24.24 +  val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
   24.25    val store_thm: (bstring * thm) * attribute list -> theory -> thm * theory
   24.26    val smart_store_thms: (bstring * thm list) -> thm list
   24.27    val smart_store_thms_open: (bstring * thm list) -> thm list
   24.28 @@ -106,12 +109,8 @@
   24.29  
   24.30  (* add / delete tags *)
   24.31  
   24.32 -fun map_tags f thm =
   24.33 -  let val (name, tags) = Thm.get_name_tags thm
   24.34 -  in Thm.put_name_tags (name, f tags) thm end;
   24.35 -
   24.36 -fun tag_rule tg = map_tags (fn tgs => if member (op =) tgs tg then tgs else tgs @ [tg]);
   24.37 -fun untag_rule s = map_tags (filter_out (fn (s', _) => s = s'));
   24.38 +fun tag_rule tg = Thm.map_tags (insert (op =) tg);
   24.39 +fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s'));
   24.40  
   24.41  fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x;
   24.42  fun untag s x = Thm.rule_attribute (K (untag_rule s)) x;
   24.43 @@ -119,18 +118,28 @@
   24.44  fun simple_tag name x = tag (name, []) x;
   24.45  
   24.46  
   24.47 +(* unofficial theorem names *)
   24.48 +
   24.49 +fun put_name_hint name = untag_rule "name" #> tag_rule ("name", [name]);
   24.50 +
   24.51 +fun get_name_hint thm =
   24.52 +  (case AList.lookup (op =) (Thm.get_tags thm) "name" of
   24.53 +    SOME (k :: _) => k
   24.54 +  | _ => "??.unknown");
   24.55 +
   24.56 +
   24.57  (* theorem kinds *)
   24.58  
   24.59  fun get_kind thm =
   24.60 -  (case AList.lookup (op =) ((#2 o Thm.get_name_tags) thm) "kind" of
   24.61 +  (case AList.lookup (op =) (Thm.get_tags thm) "kind" of
   24.62      SOME (k :: _) => k
   24.63 -  | _ => "unknown");
   24.64 +  | _ => "??.unknown");
   24.65  
   24.66  fun kind_rule k = tag_rule ("kind", [k]) o untag_rule "kind";
   24.67  fun kind k x = if k = "" then x else Thm.rule_attribute (K (kind_rule k)) x;
   24.68  fun kind_internal x = kind internalK x;
   24.69  fun has_internal tags = exists (fn ("kind", [k]) => k = internalK | _ => false) tags;
   24.70 -val is_internal = has_internal o Thm.tags_of_thm;
   24.71 +val is_internal = has_internal o Thm.get_tags;
   24.72  
   24.73  
   24.74  
   24.75 @@ -288,14 +297,14 @@
   24.76  
   24.77  fun thms_containing_consts thy consts =
   24.78    thms_containing thy (consts, []) |> maps #2
   24.79 -  |> map (fn th => (Thm.name_of_thm th, th));
   24.80 +  |> map (`(get_name_hint));
   24.81  
   24.82  
   24.83  (* thms_of etc. *)
   24.84  
   24.85  fun thms_of thy =
   24.86    let val thms = #2 (theorems_of thy)
   24.87 -  in map (fn th => (Thm.name_of_thm th, th)) (maps snd (Symtab.dest thms)) end;
   24.88 +  in map (`(get_name_hint)) (maps snd (Symtab.dest thms)) end;
   24.89  
   24.90  fun all_thms_of thy = maps thms_of (thy :: Theory.ancestors_of thy);
   24.91  
   24.92 @@ -327,12 +336,15 @@
   24.93  fun name_multi name [x] = [(name, x)]
   24.94    | name_multi name xs = gen_names 0 (length xs) name ~~ xs;
   24.95  
   24.96 -fun name_thm pre (name, thm) =
   24.97 -  if Thm.name_of_thm thm <> "" andalso pre then thm else Thm.name_thm (name, thm);
   24.98 +fun name_thm pre official name thm = thm
   24.99 +  |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)
  24.100 +  |> (if get_name_hint thm <> "" andalso pre orelse name = "" then I else put_name_hint name);
  24.101  
  24.102 -fun name_thms pre name xs = map (name_thm pre) (name_multi name xs);
  24.103 +fun name_thms pre official name xs =
  24.104 +  map (uncurry (name_thm pre official)) (name_multi name xs);
  24.105  
  24.106 -fun name_thmss name fact = burrow_fact (name_thms true name) fact;
  24.107 +fun name_thmss official name fact =
  24.108 +  burrow_fact (name_thms true official name) fact;
  24.109  
  24.110  
  24.111  (* enter_thms *)
  24.112 @@ -363,7 +375,8 @@
  24.113  (* add_thms(s) *)
  24.114  
  24.115  fun add_thms_atts pre_name ((bname, thms), atts) =
  24.116 -  enter_thms pre_name (name_thms false) (foldl_map (Thm.theory_attributes atts)) (bname, thms);
  24.117 +  enter_thms pre_name (name_thms false true)
  24.118 +    (foldl_map (Thm.theory_attributes atts)) (bname, thms);
  24.119  
  24.120  fun gen_add_thmss pre_name =
  24.121    fold_map (add_thms_atts pre_name);
  24.122 @@ -371,8 +384,8 @@
  24.123  fun gen_add_thms pre_name args =
  24.124    apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
  24.125  
  24.126 -val add_thmss = gen_add_thmss (name_thms true);
  24.127 -val add_thms = gen_add_thms (name_thms true);
  24.128 +val add_thmss = gen_add_thmss (name_thms true true);
  24.129 +val add_thms = gen_add_thms (name_thms true true);
  24.130  
  24.131  
  24.132  (* note_thmss(_i) *)
  24.133 @@ -383,7 +396,7 @@
  24.134    let
  24.135      fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
  24.136      val (thms, thy') = thy |> enter_thms
  24.137 -      name_thmss (name_thms false) (apsnd flat o foldl_map app)
  24.138 +      (name_thmss true) (name_thms false true) (apsnd flat o foldl_map app)
  24.139        (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind k])) ths_atts);
  24.140    in ((bname, thms), thy') end);
  24.141  
  24.142 @@ -405,7 +418,7 @@
  24.143  (* store_thm *)
  24.144  
  24.145  fun store_thm ((bname, thm), atts) thy =
  24.146 -  let val ([th'], thy') = add_thms_atts (name_thms true) ((bname, [thm]), atts) thy
  24.147 +  let val ([th'], thy') = add_thms_atts (name_thms true true) ((bname, [thm]), atts) thy
  24.148    in (th', thy') end;
  24.149  
  24.150  
  24.151 @@ -415,16 +428,18 @@
  24.152  
  24.153  fun smart_store _ (name, []) =
  24.154        error ("Cannot store empty list of theorems: " ^ quote name)
  24.155 -  | smart_store name_thm (name, [thm]) =
  24.156 -      fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
  24.157 -  | smart_store name_thm (name, thms) =
  24.158 -      let val thy = Theory.merge_list (map Thm.theory_of_thm thms)
  24.159 -      in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
  24.160 +  | smart_store official (name, [thm]) =
  24.161 +      fst (enter_thms (name_thms true official) (name_thms false official) I (name, [thm])
  24.162 +        (Thm.theory_of_thm thm))
  24.163 +  | smart_store official (name, thms) =
  24.164 +      let val thy = Theory.merge_list (map Thm.theory_of_thm thms) in
  24.165 +        fst (enter_thms (name_thms true official) (name_thms false official) I (name, thms) thy)
  24.166 +      end;
  24.167  
  24.168  in
  24.169  
  24.170 -val smart_store_thms = smart_store name_thms;
  24.171 -val smart_store_thms_open = smart_store (K (K I));
  24.172 +val smart_store_thms = smart_store true;
  24.173 +val smart_store_thms_open = smart_store false;
  24.174  
  24.175  end;
  24.176  
    25.1 --- a/src/Pure/thm.ML	Tue Dec 05 00:29:19 2006 +0100
    25.2 +++ b/src/Pure/thm.ML	Tue Dec 05 00:30:38 2006 +0100
    25.3 @@ -55,6 +55,7 @@
    25.4     {thy: theory,
    25.5      sign: theory,       (*obsolete*)
    25.6      der: bool * Proofterm.proof,
    25.7 +    tags: tag list,
    25.8      maxidx: int,
    25.9      shyps: sort list,
   25.10      hyps: term list,
   25.11 @@ -64,6 +65,7 @@
   25.12     {thy: theory,
   25.13      sign: theory,       (*obsolete*)
   25.14      der: bool * Proofterm.proof,
   25.15 +    tags: tag list,
   25.16      maxidx: int,
   25.17      shyps: sort list,
   25.18      hyps: cterm list,
   25.19 @@ -161,11 +163,10 @@
   25.20    val maxidx_thm: thm -> int -> int
   25.21    val hyps_of: thm -> term list
   25.22    val full_prop_of: thm -> term
   25.23 -  val get_name_tags: thm -> string * tag list
   25.24 -  val put_name_tags: string * tag list -> thm -> thm
   25.25 -  val name_of_thm: thm -> string
   25.26 -  val tags_of_thm: thm -> tag list
   25.27 -  val name_thm: string * thm -> thm
   25.28 +  val get_name: thm -> string
   25.29 +  val put_name: string -> thm -> thm
   25.30 +  val get_tags: thm -> tag list
   25.31 +  val map_tags: (tag list -> tag list) -> thm -> thm
   25.32    val compress: thm -> thm
   25.33    val adjust_maxidx_thm: int -> thm -> thm
   25.34    val rename_boundvars: term -> term -> thm -> thm
   25.35 @@ -376,17 +377,17 @@
   25.36  fun read_cterm thy = #1 o read_def_cterm (thy, K NONE, K NONE) [] true;
   25.37  
   25.38  
   25.39 -(*tags provide additional comment, apart from the axiom/theorem name*)
   25.40 -type tag = string * string list;
   25.41 -
   25.42  
   25.43  (*** Meta theorems ***)
   25.44  
   25.45  structure Pt = Proofterm;
   25.46  
   25.47 +type tag = string * string list;
   25.48 +
   25.49  datatype thm = Thm of
   25.50   {thy_ref: theory_ref,         (*dynamic reference to theory*)
   25.51    der: bool * Pt.proof,        (*derivation*)
   25.52 +  tags: tag list,              (*additional annotations/comments*)
   25.53    maxidx: int,                 (*maximum index of any Var or TVar*)
   25.54    shyps: sort list,            (*sort hypotheses as ordered list*)
   25.55    hyps: term list,             (*hypotheses as ordered list*)
   25.56 @@ -396,19 +397,19 @@
   25.57  (*errors involving theorems*)
   25.58  exception THM of string * int * thm list;
   25.59  
   25.60 -fun rep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   25.61 +fun rep_thm (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   25.62    let val thy = Theory.deref thy_ref in
   25.63 -   {thy = thy, sign = thy, der = der, maxidx = maxidx,
   25.64 +   {thy = thy, sign = thy, der = der, tags = tags, maxidx = maxidx,
   25.65      shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}
   25.66    end;
   25.67  
   25.68  (*version of rep_thm returning cterms instead of terms*)
   25.69 -fun crep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   25.70 +fun crep_thm (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   25.71    let
   25.72      val thy = Theory.deref thy_ref;
   25.73      fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps};
   25.74    in
   25.75 -   {thy = thy, sign = thy, der = der, maxidx = maxidx, shyps = shyps,
   25.76 +   {thy = thy, sign = thy, der = der, tags = tags, maxidx = maxidx, shyps = shyps,
   25.77      hyps = map (cterm ~1) hyps,
   25.78      tpairs = map (pairself (cterm maxidx)) tpairs,
   25.79      prop = cterm maxidx prop}
   25.80 @@ -519,7 +520,7 @@
   25.81  (*explicit transfer to a super theory*)
   25.82  fun transfer thy' thm =
   25.83    let
   25.84 -    val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm;
   25.85 +    val Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop} = thm;
   25.86      val thy = Theory.deref thy_ref;
   25.87    in
   25.88      if not (subthy (thy, thy')) then
   25.89 @@ -528,6 +529,7 @@
   25.90      else
   25.91        Thm {thy_ref = Theory.self_ref thy',
   25.92          der = der,
   25.93 +        tags = tags,
   25.94          maxidx = maxidx,
   25.95          shyps = shyps,
   25.96          hyps = hyps,
   25.97 @@ -539,7 +541,7 @@
   25.98  fun weaken raw_ct th =
   25.99    let
  25.100      val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct;
  25.101 -    val Thm {der, maxidx, shyps, hyps, tpairs, prop, ...} = th;
  25.102 +    val Thm {der, tags, maxidx, shyps, hyps, tpairs, prop, ...} = th;
  25.103    in
  25.104      if T <> propT then
  25.105        raise THM ("weaken: assumptions must have type prop", 0, [])
  25.106 @@ -548,6 +550,7 @@
  25.107      else
  25.108        Thm {thy_ref = merge_thys1 ct th,
  25.109          der = der,
  25.110 +        tags = tags,
  25.111          maxidx = maxidx,
  25.112          shyps = Sorts.union sorts shyps,
  25.113          hyps = insert_hyps A hyps,
  25.114 @@ -565,7 +568,7 @@
  25.115  
  25.116  (*remove extra sorts that are non-empty by virtue of type signature information*)
  25.117  fun strip_shyps (thm as Thm {shyps = [], ...}) = thm
  25.118 -  | strip_shyps (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  25.119 +  | strip_shyps (thm as Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
  25.120        let
  25.121          val thy = Theory.deref thy_ref;
  25.122          val shyps' =
  25.123 @@ -577,7 +580,7 @@
  25.124                val witnessed = map #2 (Sign.witness_sorts thy present extra);
  25.125              in Sorts.subtract witnessed shyps end;
  25.126        in
  25.127 -        Thm {thy_ref = thy_ref, der = der, maxidx = maxidx,
  25.128 +        Thm {thy_ref = thy_ref, der = der, tags = tags, maxidx = maxidx,
  25.129            shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}
  25.130        end;
  25.131  
  25.132 @@ -596,6 +599,7 @@
  25.133        |> Option.map (fn prop =>
  25.134            Thm {thy_ref = Theory.self_ref thy,
  25.135              der = Pt.infer_derivs' I (false, Pt.axm_proof name prop),
  25.136 +            tags = [],
  25.137              maxidx = maxidx_of_term prop,
  25.138              shyps = may_insert_term_sorts thy prop [],
  25.139              hyps = [],
  25.140 @@ -624,30 +628,31 @@
  25.141      (Symtab.dest (#2 (#axioms (Theory.rep_theory thy))));
  25.142  
  25.143  
  25.144 -(* name and tags -- make proof objects more readable *)
  25.145 +(* official name and additional tags *)
  25.146  
  25.147 -fun get_name_tags (Thm {hyps, prop, der = (_, prf), ...}) =
  25.148 -  Pt.get_name_tags hyps prop prf;
  25.149 +fun get_name (Thm {hyps, prop, der = (_, prf), ...}) =
  25.150 +  Pt.get_name hyps prop prf;
  25.151  
  25.152 -fun put_name_tags x (Thm {thy_ref, der = (ora, prf), maxidx,
  25.153 -      shyps, hyps, tpairs = [], prop}) = Thm {thy_ref = thy_ref,
  25.154 -        der = (ora, Pt.thm_proof (Theory.deref thy_ref) x hyps prop prf),
  25.155 -        maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = [], prop = prop}
  25.156 -  | put_name_tags _ thm =
  25.157 -      raise THM ("put_name_tags: unsolved flex-flex constraints", 0, [thm]);
  25.158 +fun put_name name (Thm {thy_ref, der = (ora, prf), tags, maxidx, shyps, hyps, tpairs = [], prop}) =
  25.159 +      Thm {thy_ref = thy_ref,
  25.160 +        der = (ora, Pt.thm_proof (Theory.deref thy_ref) name hyps prop prf),
  25.161 +        tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = [], prop = prop}
  25.162 +  | put_name _ thm = raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
  25.163  
  25.164 -val name_of_thm = #1 o get_name_tags;
  25.165 -val tags_of_thm = #2 o get_name_tags;
  25.166 +val get_tags = #tags o rep_thm;
  25.167  
  25.168 -fun name_thm (name, thm) = put_name_tags (name, tags_of_thm thm) thm;
  25.169 +fun map_tags f (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
  25.170 +  Thm {thy_ref = thy_ref, der = der, tags = f tags, maxidx = maxidx,
  25.171 +    shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop};
  25.172  
  25.173  
  25.174  (*Compression of theorems -- a separate rule, not integrated with the others,
  25.175    as it could be slow.*)
  25.176 -fun compress (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  25.177 +fun compress (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
  25.178    let val thy = Theory.deref thy_ref in
  25.179      Thm {thy_ref = thy_ref,
  25.180        der = der,
  25.181 +      tags = tags,
  25.182        maxidx = maxidx,
  25.183        shyps = shyps,
  25.184        hyps = map (Compress.term thy) hyps,
  25.185 @@ -655,14 +660,14 @@
  25.186        prop = Compress.term thy prop}
  25.187    end;
  25.188  
  25.189 -fun adjust_maxidx_thm i (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  25.190 +fun adjust_maxidx_thm i (th as Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
  25.191    if maxidx = i then th
  25.192    else if maxidx < i then
  25.193 -    Thm {maxidx = i, thy_ref = thy_ref, der = der, shyps = shyps,
  25.194 +    Thm {maxidx = i, thy_ref = thy_ref, der = der, tags = tags, shyps = shyps,
  25.195        hyps = hyps, tpairs = tpairs, prop = prop}
  25.196    else
  25.197 -    Thm {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i),
  25.198 -      thy_ref = thy_ref, der = der, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop};
  25.199 +    Thm {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), thy_ref = thy_ref,
  25.200 +      der = der, tags = tags, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop};
  25.201  
  25.202  
  25.203  
  25.204 @@ -679,6 +684,7 @@
  25.205        raise THM ("assume: variables", maxidx, [])
  25.206      else Thm {thy_ref = thy_ref,
  25.207        der = Pt.infer_derivs' I (false, Pt.Hyp prop),
  25.208 +      tags = [],
  25.209        maxidx = ~1,
  25.210        shyps = sorts,
  25.211        hyps = [prop],
  25.212 @@ -701,6 +707,7 @@
  25.213    else
  25.214      Thm {thy_ref = merge_thys1 ct th,
  25.215        der = Pt.infer_derivs' (Pt.implies_intr_proof A) der,
  25.216 +      tags = [],
  25.217        maxidx = Int.max (maxidxA, maxidx),
  25.218        shyps = Sorts.union sorts shyps,
  25.219        hyps = remove_hyps A hyps,
  25.220 @@ -725,6 +732,7 @@
  25.221          if A aconv propA then
  25.222            Thm {thy_ref = merge_thys2 thAB thA,
  25.223              der = Pt.infer_derivs (curry Pt.%%) der derA,
  25.224 +            tags = [],
  25.225              maxidx = Int.max (maxA, maxidx),
  25.226              shyps = Sorts.union shypsA shyps,
  25.227              hyps = union_hyps hypsA hyps,
  25.228 @@ -748,6 +756,7 @@
  25.229      fun result a =
  25.230        Thm {thy_ref = merge_thys1 ct th,
  25.231          der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der,
  25.232 +        tags = [],
  25.233          maxidx = maxidx,
  25.234          shyps = Sorts.union sorts shyps,
  25.235          hyps = hyps,
  25.236 @@ -779,6 +788,7 @@
  25.237        else
  25.238          Thm {thy_ref = merge_thys1 ct th,
  25.239            der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der,
  25.240 +          tags = [],
  25.241            maxidx = Int.max (maxidx, maxt),
  25.242            shyps = Sorts.union sorts shyps,
  25.243            hyps = hyps,
  25.244 @@ -795,6 +805,7 @@
  25.245  fun reflexive (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =
  25.246    Thm {thy_ref = thy_ref,
  25.247      der = Pt.infer_derivs' I (false, Pt.reflexive),
  25.248 +    tags = [],
  25.249      maxidx = maxidx,
  25.250      shyps = sorts,
  25.251      hyps = [],
  25.252 @@ -806,11 +817,12 @@
  25.253    ------
  25.254    u == t
  25.255  *)
  25.256 -fun symmetric (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  25.257 +fun symmetric (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
  25.258    (case prop of
  25.259      (eq as Const ("==", Type (_, [T, _]))) $ t $ u =>
  25.260        Thm {thy_ref = thy_ref,
  25.261          der = Pt.infer_derivs' Pt.symmetric der,
  25.262 +        tags = [],
  25.263          maxidx = maxidx,
  25.264          shyps = shyps,
  25.265          hyps = hyps,
  25.266 @@ -837,6 +849,7 @@
  25.267          else
  25.268            Thm {thy_ref = merge_thys2 th1 th2,
  25.269              der = Pt.infer_derivs (Pt.transitive u T) der1 der2,
  25.270 +            tags = [],
  25.271              maxidx = Int.max (max1, max2),
  25.272              shyps = Sorts.union shyps1 shyps2,
  25.273              hyps = union_hyps hyps1 hyps2,
  25.274 @@ -858,6 +871,7 @@
  25.275    in
  25.276      Thm {thy_ref = thy_ref,
  25.277        der = Pt.infer_derivs' I (false, Pt.reflexive),
  25.278 +      tags = [],
  25.279        maxidx = maxidx,
  25.280        shyps = sorts,
  25.281        hyps = [],
  25.282 @@ -868,6 +882,7 @@
  25.283  fun eta_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
  25.284    Thm {thy_ref = thy_ref,
  25.285      der = Pt.infer_derivs' I (false, Pt.reflexive),
  25.286 +    tags = [],
  25.287      maxidx = maxidx,
  25.288      shyps = sorts,
  25.289      hyps = [],
  25.290 @@ -882,7 +897,7 @@
  25.291  *)
  25.292  fun abstract_rule a
  25.293      (Cterm {t = x, T, sorts, ...})
  25.294 -    (th as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) =
  25.295 +    (th as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop, ...}) =
  25.296    let
  25.297      val string_of = Sign.string_of_term (Theory.deref thy_ref);
  25.298      val (t, u) = Logic.dest_equals prop
  25.299 @@ -890,6 +905,7 @@
  25.300      val result =
  25.301        Thm {thy_ref = thy_ref,
  25.302          der = Pt.infer_derivs' (Pt.abstract_rule x a) der,
  25.303 +        tags = [],
  25.304          maxidx = maxidx,
  25.305          shyps = Sorts.union sorts shyps,
  25.306          hyps = hyps,
  25.307 @@ -932,6 +948,7 @@
  25.308          (chktypes fT tT;
  25.309            Thm {thy_ref = merge_thys2 th1 th2,
  25.310              der = Pt.infer_derivs (Pt.combination f g t u fT) der1 der2,
  25.311 +            tags = [],
  25.312              maxidx = Int.max (max1, max2),
  25.313              shyps = Sorts.union shyps1 shyps2,
  25.314              hyps = union_hyps hyps1 hyps2,
  25.315 @@ -958,6 +975,7 @@
  25.316          if A aconv A' andalso B aconv B' then
  25.317            Thm {thy_ref = merge_thys2 th1 th2,
  25.318              der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2,
  25.319 +            tags = [],
  25.320              maxidx = Int.max (max1, max2),
  25.321              shyps = Sorts.union shyps1 shyps2,
  25.322              hyps = union_hyps hyps1 hyps2,
  25.323 @@ -985,6 +1003,7 @@
  25.324          if prop2 aconv A then
  25.325            Thm {thy_ref = merge_thys2 th1 th2,
  25.326              der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2,
  25.327 +            tags = [],
  25.328              maxidx = Int.max (max1, max2),
  25.329              shyps = Sorts.union shyps1 shyps2,
  25.330              hyps = union_hyps hyps1 hyps2,
  25.331 @@ -1002,7 +1021,7 @@
  25.332    Instantiates the theorem and deletes trivial tpairs.
  25.333    Resulting sequence may contain multiple elements if the tpairs are
  25.334      not all flex-flex. *)
  25.335 -fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  25.336 +fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
  25.337    Unify.smash_unifiers (Theory.deref thy_ref) tpairs (Envir.empty maxidx)
  25.338    |> Seq.map (fn env =>
  25.339        if Envir.is_empty env then th
  25.340 @@ -1015,6 +1034,7 @@
  25.341          in
  25.342            Thm {thy_ref = thy_ref,
  25.343              der = Pt.infer_derivs' (Pt.norm_proof' env) der,
  25.344 +            tags = [],
  25.345              maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'),
  25.346              shyps = may_insert_env_sorts (Theory.deref thy_ref) env shyps,
  25.347              hyps = hyps,
  25.348 @@ -1032,7 +1052,7 @@
  25.349  fun generalize ([], []) _ th = th
  25.350    | generalize (tfrees, frees) idx th =
  25.351        let
  25.352 -        val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = th;
  25.353 +        val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...} = th;
  25.354          val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]);
  25.355  
  25.356          val bad_type = if null tfrees then K false else
  25.357 @@ -1054,6 +1074,7 @@
  25.358          Thm {
  25.359            thy_ref = thy_ref,
  25.360            der = Pt.infer_derivs' (Pt.generalize (tfrees, frees) idx) der,
  25.361 +          tags = [],
  25.362            maxidx = maxidx',
  25.363            shyps = shyps,
  25.364            hyps = hyps,
  25.365 @@ -1126,6 +1147,7 @@
  25.366          Thm {thy_ref = thy_ref',
  25.367            der = Pt.infer_derivs' (fn d =>
  25.368              Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
  25.369 +          tags = [],
  25.370            maxidx = maxidx',
  25.371            shyps = shyps',
  25.372            hyps = hyps,
  25.373 @@ -1145,6 +1167,7 @@
  25.374    else
  25.375      Thm {thy_ref = thy_ref,
  25.376        der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)),
  25.377 +      tags = [],
  25.378        maxidx = maxidx,
  25.379        shyps = sorts,
  25.380        hyps = [],
  25.381 @@ -1159,6 +1182,7 @@
  25.382    in
  25.383      Thm {thy_ref = thy_ref,
  25.384        der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])),
  25.385 +      tags = [],
  25.386        maxidx = maxidx,
  25.387        shyps = sorts,
  25.388        hyps = [],
  25.389 @@ -1169,7 +1193,7 @@
  25.390  (*Internalize sort constraints of type variable*)
  25.391  fun unconstrainT
  25.392      (Ctyp {thy_ref = thy_ref1, T, ...})
  25.393 -    (th as Thm {thy_ref = thy_ref2, der, maxidx, shyps, hyps, tpairs, prop}) =
  25.394 +    (th as Thm {thy_ref = thy_ref2, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
  25.395    let
  25.396      val ((x, i), S) = Term.dest_TVar T handle TYPE _ =>
  25.397        raise THM ("unconstrainT: not a type variable", 0, [th]);
  25.398 @@ -1179,6 +1203,7 @@
  25.399    in
  25.400      Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
  25.401        der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.unconstrainT", prop, SOME [])),
  25.402 +      tags = [],
  25.403        maxidx = Int.max (maxidx, i),
  25.404        shyps = Sorts.remove_sort S shyps,
  25.405        hyps = hyps,
  25.406 @@ -1187,7 +1212,7 @@
  25.407    end;
  25.408  
  25.409  (* Replace all TFrees not fixed or in the hyps by new TVars *)
  25.410 -fun varifyT' fixed (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  25.411 +fun varifyT' fixed (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
  25.412    let
  25.413      val tfrees = foldr add_term_tfrees fixed hyps;
  25.414      val prop1 = attach_tpairs tpairs prop;
  25.415 @@ -1196,6 +1221,7 @@
  25.416    in
  25.417      (al, Thm {thy_ref = thy_ref,
  25.418        der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der,
  25.419 +      tags = [],
  25.420        maxidx = Int.max (0, maxidx),
  25.421        shyps = shyps,
  25.422        hyps = hyps,
  25.423 @@ -1206,7 +1232,7 @@
  25.424  val varifyT = #2 o varifyT' [];
  25.425  
  25.426  (* Replace all TVars by new TFrees *)
  25.427 -fun freezeT (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  25.428 +fun freezeT (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
  25.429    let
  25.430      val prop1 = attach_tpairs tpairs prop;
  25.431      val prop2 = Type.freeze prop1;
  25.432 @@ -1214,6 +1240,7 @@
  25.433    in
  25.434      Thm {thy_ref = thy_ref,
  25.435        der = Pt.infer_derivs' (Pt.freezeT prop1) der,
  25.436 +      tags = [],
  25.437        maxidx = maxidx_of_term prop2,
  25.438        shyps = shyps,
  25.439        hyps = hyps,
  25.440 @@ -1246,6 +1273,7 @@
  25.441      else
  25.442        Thm {thy_ref = merge_thys1 goal orule,
  25.443          der = Pt.infer_derivs' (Pt.lift_proof gprop inc prop) der,
  25.444 +        tags = [],
  25.445          maxidx = maxidx + inc,
  25.446          shyps = Sorts.union shyps sorts,  (*sic!*)
  25.447          hyps = hyps,
  25.448 @@ -1253,13 +1281,14 @@
  25.449          prop = Logic.list_implies (map lift_all As, lift_all B)}
  25.450    end;
  25.451  
  25.452 -fun incr_indexes i (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  25.453 +fun incr_indexes i (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
  25.454    if i < 0 then raise THM ("negative increment", 0, [thm])
  25.455    else if i = 0 then thm
  25.456    else
  25.457      Thm {thy_ref = thy_ref,
  25.458        der = Pt.infer_derivs'
  25.459          (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der,
  25.460 +      tags = [],
  25.461        maxidx = maxidx + i,
  25.462        shyps = shyps,
  25.463        hyps = hyps,
  25.464 @@ -1277,6 +1306,7 @@
  25.465          der = Pt.infer_derivs'
  25.466            ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
  25.467              Pt.assumption_proof Bs Bi n) der,
  25.468 +        tags = [],
  25.469          maxidx = maxidx,
  25.470          shyps = may_insert_env_sorts thy env shyps,
  25.471          hyps = hyps,
  25.472 @@ -1307,6 +1337,7 @@
  25.473      | n =>
  25.474          Thm {thy_ref = thy_ref,
  25.475            der = Pt.infer_derivs' (Pt.assumption_proof Bs Bi (n + 1)) der,
  25.476 +          tags = [],
  25.477            maxidx = maxidx,
  25.478            shyps = shyps,
  25.479            hyps = hyps,
  25.480 @@ -1335,6 +1366,7 @@
  25.481    in
  25.482      Thm {thy_ref = thy_ref,
  25.483        der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der,
  25.484 +      tags = [],
  25.485        maxidx = maxidx,
  25.486        shyps = shyps,
  25.487        hyps = hyps,
  25.488 @@ -1348,7 +1380,7 @@
  25.489    number of premises.  Useful with etac and underlies defer_tac*)
  25.490  fun permute_prems j k rl =
  25.491    let
  25.492 -    val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = rl;
  25.493 +    val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...} = rl;
  25.494      val prems = Logic.strip_imp_prems prop
  25.495      and concl = Logic.strip_imp_concl prop;
  25.496      val moved_prems = List.drop (prems, j)
  25.497 @@ -1365,6 +1397,7 @@
  25.498    in
  25.499      Thm {thy_ref = thy_ref,
  25.500        der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der,
  25.501 +      tags = [],
  25.502        maxidx = maxidx,
  25.503        shyps = shyps,
  25.504        hyps = hyps,
  25.505 @@ -1381,7 +1414,7 @@
  25.506    preceding parameters may be renamed to make all params distinct.*)
  25.507  fun rename_params_rule (cs, i) state =
  25.508    let
  25.509 -    val Thm {thy_ref, der, maxidx, shyps, hyps, ...} = state;
  25.510 +    val Thm {thy_ref, der, tags, maxidx, shyps, hyps, ...} = state;
  25.511      val (tpairs, Bs, Bi, C) = dest_state (state, i);
  25.512      val iparams = map #1 (Logic.strip_params Bi);
  25.513      val short = length iparams - length cs;
  25.514 @@ -1399,6 +1432,7 @@
  25.515        | [] =>
  25.516          Thm {thy_ref = thy_ref,
  25.517            der = der,
  25.518 +          tags = tags,
  25.519            maxidx = maxidx,
  25.520            shyps = shyps,
  25.521            hyps = hyps,
  25.522 @@ -1409,12 +1443,13 @@
  25.523  
  25.524  (*** Preservation of bound variable names ***)
  25.525  
  25.526 -fun rename_boundvars pat obj (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  25.527 +fun rename_boundvars pat obj (thm as Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
  25.528    (case Term.rename_abs pat obj prop of
  25.529      NONE => thm
  25.530    | SOME prop' => Thm
  25.531        {thy_ref = thy_ref,
  25.532         der = der,
  25.533 +       tags = tags,
  25.534         maxidx = maxidx,
  25.535         hyps = hyps,
  25.536         shyps = shyps,
  25.537 @@ -1535,6 +1570,7 @@
  25.538                       else
  25.539                         curry op oo (Pt.norm_proof' env))
  25.540                      (Pt.bicompose_proof flatten Bs oldAs As A n)) rder' sder,
  25.541 +                 tags = [],
  25.542                   maxidx = maxidx,
  25.543                   shyps = may_insert_env_sorts thy env (Sorts.union rshyps sshyps),
  25.544                   hyps = union_hyps rhyps shyps,
  25.545 @@ -1632,6 +1668,7 @@
  25.546          else
  25.547            Thm {thy_ref = Theory.self_ref thy',
  25.548              der = (true, Pt.oracle_proof name prop),
  25.549 +            tags = [],
  25.550              maxidx = maxidx,
  25.551              shyps = may_insert_term_sorts thy' prop [],
  25.552              hyps = [],