renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
authorwenzelm
Sat May 08 16:53:53 2010 +0200 (2010-05-08)
changeset 367446e1f3d609a68
parent 36743 ce2297415b54
child 36745 403585a89772
renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/inductive_realizer.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Thy/thm_deps.ML
src/Pure/more_thm.ML
src/Pure/pure_thy.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat May 08 17:10:27 2010 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat May 08 16:53:53 2010 +0200
     1.3 @@ -120,7 +120,7 @@
     1.4            REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
     1.5              REPEAT (etac allE i) THEN atac i)) 1)]);
     1.6  
     1.7 -    val ind_name = Thm.get_name induct;
     1.8 +    val ind_name = Thm.derivation_name induct;
     1.9      val vs = map (fn i => List.nth (pnames, i)) is;
    1.10      val (thm', thy') = thy
    1.11        |> Sign.root_path
    1.12 @@ -191,7 +191,7 @@
    1.13              [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
    1.14               resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
    1.15  
    1.16 -    val exh_name = Thm.get_name exhaust;
    1.17 +    val exh_name = Thm.derivation_name exhaust;
    1.18      val (thm', thy') = thy
    1.19        |> Sign.root_path
    1.20        |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
     2.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat May 08 17:10:27 2010 +0200
     2.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat May 08 16:53:53 2010 +0200
     2.3 @@ -408,7 +408,7 @@
     2.4        in
     2.5          Extraction.add_realizers_i
     2.6            (map (fn (((ind, corr), rlz), r) =>
     2.7 -              mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
     2.8 +              mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
     2.9              realizers @ (case realizers of
    2.10               [(((ind, corr), rlz), r)] =>
    2.11                 [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
     3.1 --- a/src/Pure/Proof/extraction.ML	Sat May 08 17:10:27 2010 +0200
     3.2 +++ b/src/Pure/Proof/extraction.ML	Sat May 08 16:53:53 2010 +0200
     3.3 @@ -303,7 +303,7 @@
     3.4      val rd = Proof_Syntax.read_proof thy' false;
     3.5    in fn (thm, (vs, s1, s2)) =>
     3.6      let
     3.7 -      val name = Thm.get_name thm;
     3.8 +      val name = Thm.derivation_name thm;
     3.9        val _ = name <> "" orelse error "add_realizers: unnamed theorem";
    3.10        val prop = Pattern.rewrite_term thy'
    3.11          (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
    3.12 @@ -348,7 +348,7 @@
    3.13      val {realizes_eqns, typeof_eqns, types, realizers,
    3.14        defs, expand, prep} = ExtractionData.get thy;
    3.15  
    3.16 -    val name = Thm.get_name thm;
    3.17 +    val name = Thm.derivation_name thm;
    3.18      val _ = name <> "" orelse error "add_expand_thm: unnamed theorem";
    3.19    in
    3.20      thy |> ExtractionData.put
    3.21 @@ -706,7 +706,7 @@
    3.22          val thy = Thm.theory_of_thm thm;
    3.23          val prop = Thm.prop_of thm;
    3.24          val prf = Thm.proof_of thm;
    3.25 -        val name = Thm.get_name thm;
    3.26 +        val name = Thm.derivation_name thm;
    3.27          val _ = name <> "" orelse error "extraction: unnamed theorem";
    3.28          val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
    3.29            quote name ^ " has no computational content")
     4.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Sat May 08 17:10:27 2010 +0200
     4.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sat May 08 16:53:53 2010 +0200
     4.3 @@ -244,7 +244,7 @@
     4.4  fun elim_defs thy r defs prf =
     4.5    let
     4.6      val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
     4.7 -    val defnames = map Thm.get_name defs;
     4.8 +    val defnames = map Thm.derivation_name defs;
     4.9      val f = if not r then I else
    4.10        let
    4.11          val cnames = map (fst o dest_Const o fst) defs';
     5.1 --- a/src/Pure/Thy/thm_deps.ML	Sat May 08 17:10:27 2010 +0200
     5.2 +++ b/src/Pure/Thy/thm_deps.ML	Sat May 08 16:53:53 2010 +0200
     5.3 @@ -53,7 +53,7 @@
     5.4        else
     5.5          let val {concealed, group, ...} = Name_Space.the_entry space name in
     5.6            fold_rev (fn th =>
     5.7 -            (case Thm.get_name th of
     5.8 +            (case Thm.derivation_name th of
     5.9                "" => I
    5.10              | a => cons (a, (th, concealed, group)))) ths
    5.11          end;
     6.1 --- a/src/Pure/more_thm.ML	Sat May 08 17:10:27 2010 +0200
     6.2 +++ b/src/Pure/more_thm.ML	Sat May 08 16:53:53 2010 +0200
     6.3 @@ -326,7 +326,7 @@
     6.4  (* close_derivation *)
     6.5  
     6.6  fun close_derivation thm =
     6.7 -  if Thm.get_name thm = "" then Thm.put_name "" thm
     6.8 +  if Thm.derivation_name thm = "" then Thm.name_derivation "" thm
     6.9    else thm;
    6.10  
    6.11  
     7.1 --- a/src/Pure/pure_thy.ML	Sat May 08 17:10:27 2010 +0200
     7.2 +++ b/src/Pure/pure_thy.ML	Sat May 08 16:53:53 2010 +0200
     7.3 @@ -121,7 +121,7 @@
     7.4    | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
     7.5  
     7.6  fun name_thm pre official name thm = thm
     7.7 -  |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)
     7.8 +  |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name
     7.9    |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name);
    7.10  
    7.11  fun name_thms pre official name xs =
     8.1 --- a/src/Pure/thm.ML	Sat May 08 17:10:27 2010 +0200
     8.2 +++ b/src/Pure/thm.ML	Sat May 08 16:53:53 2010 +0200
     8.3 @@ -126,8 +126,8 @@
     8.4    val proof_of: thm -> proof
     8.5    val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
     8.6    val future: thm future -> cterm -> thm
     8.7 -  val get_name: thm -> string
     8.8 -  val put_name: string -> thm -> thm
     8.9 +  val derivation_name: thm -> string
    8.10 +  val name_derivation: string -> thm -> thm
    8.11    val axiom: theory -> string -> thm
    8.12    val axioms_of: theory -> (string * thm) list
    8.13    val get_tags: thm -> Properties.T
    8.14 @@ -585,10 +585,10 @@
    8.15  
    8.16  (* closed derivations with official name *)
    8.17  
    8.18 -fun get_name thm =
    8.19 +fun derivation_name thm =
    8.20    Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
    8.21  
    8.22 -fun put_name name (thm as Thm (der, args)) =
    8.23 +fun name_derivation name (thm as Thm (der, args)) =
    8.24    let
    8.25      val Deriv {promises, body} = der;
    8.26      val {thy_ref, hyps, prop, tpairs, ...} = args;