clarified derivation_name vs. raw_derivation_name;
authorwenzelm
Fri Aug 16 10:04:47 2019 +0200 (4 days ago)
changeset 7054333749040b6f8
parent 70542 011196c029e1
child 70544 16e98f89a29c
clarified derivation_name vs. raw_derivation_name;
src/Pure/global_theory.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/global_theory.ML	Thu Aug 15 21:46:43 2019 +0200
     1.2 +++ b/src/Pure/global_theory.ML	Fri Aug 16 10:04:47 2019 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4        No_Name_Flags => thm
     1.5      | Name_Flags {pre, official} =>
     1.6          thm
     1.7 -        |> (official andalso (not pre orelse Thm.derivation_name thm = "")) ?
     1.8 +        |> (official andalso (not pre orelse Thm.raw_derivation_name thm = "")) ?
     1.9              Thm.name_derivation (name, pos)
    1.10          |> (name <> "" andalso (not pre orelse not (Thm.has_name_hint thm))) ?
    1.11              Thm.put_name_hint name));
     2.1 --- a/src/Pure/thm.ML	Thu Aug 15 21:46:43 2019 +0200
     2.2 +++ b/src/Pure/thm.ML	Fri Aug 16 10:04:47 2019 +0200
     2.3 @@ -106,6 +106,7 @@
     2.4    val future: thm future -> cterm -> thm
     2.5    val derivation_closed: thm -> bool
     2.6    val derivation_name: thm -> string
     2.7 +  val raw_derivation_name: thm -> string
     2.8    val name_derivation: string * Position.T -> thm -> thm
     2.9    val close_derivation: Position.T -> thm -> thm
    2.10    val trim_context: thm -> thm
    2.11 @@ -996,9 +997,13 @@
    2.12    Proofterm.compact_proof (Proofterm.proof_of body);
    2.13  
    2.14  (*non-deterministic, depends on unknown promises*)
    2.15 -fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
    2.16 +fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
    2.17    Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
    2.18  
    2.19 +(*deterministic name of finished proof*)
    2.20 +fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
    2.21 +  Proofterm.get_name shyps hyps prop (proof_of thm);
    2.22 +
    2.23  fun name_derivation name_pos =
    2.24    solve_constraints #> (fn thm as Thm (der, args) =>
    2.25      let