# HG changeset patch # User wenzelm # Date 1273330433 -7200 # Node ID 6e1f3d609a684f1d31073f445babf56fb7ed0799 # Parent ce2297415b5461acfec1317e5d3b457a9d379d86 renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations; diff -r ce2297415b54 -r 6e1f3d609a68 src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Sat May 08 17:10:27 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sat May 08 16:53:53 2010 +0200 @@ -120,7 +120,7 @@ REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i => REPEAT (etac allE i) THEN atac i)) 1)]); - val ind_name = Thm.get_name induct; + val ind_name = Thm.derivation_name induct; val vs = map (fn i => List.nth (pnames, i)) is; val (thm', thy') = thy |> Sign.root_path @@ -191,7 +191,7 @@ [asm_simp_tac (HOL_basic_ss addsimps case_rewrites), resolve_tac prems, asm_simp_tac HOL_basic_ss])]); - val exh_name = Thm.get_name exhaust; + val exh_name = Thm.derivation_name exhaust; val (thm', thy') = thy |> Sign.root_path |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm) diff -r ce2297415b54 -r 6e1f3d609a68 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Sat May 08 17:10:27 2010 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Sat May 08 16:53:53 2010 +0200 @@ -408,7 +408,7 @@ in Extraction.add_realizers_i (map (fn (((ind, corr), rlz), r) => - mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r)) + mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r)) realizers @ (case realizers of [(((ind, corr), rlz), r)] => [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct", diff -r ce2297415b54 -r 6e1f3d609a68 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Sat May 08 17:10:27 2010 +0200 +++ b/src/Pure/Proof/extraction.ML Sat May 08 16:53:53 2010 +0200 @@ -303,7 +303,7 @@ val rd = Proof_Syntax.read_proof thy' false; in fn (thm, (vs, s1, s2)) => let - val name = Thm.get_name thm; + val name = Thm.derivation_name thm; val _ = name <> "" orelse error "add_realizers: unnamed theorem"; val prop = Pattern.rewrite_term thy' (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm); @@ -348,7 +348,7 @@ val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} = ExtractionData.get thy; - val name = Thm.get_name thm; + val name = Thm.derivation_name thm; val _ = name <> "" orelse error "add_expand_thm: unnamed theorem"; in thy |> ExtractionData.put @@ -706,7 +706,7 @@ val thy = Thm.theory_of_thm thm; val prop = Thm.prop_of thm; val prf = Thm.proof_of thm; - val name = Thm.get_name thm; + val name = Thm.derivation_name thm; val _ = name <> "" orelse error "extraction: unnamed theorem"; val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^ quote name ^ " has no computational content") diff -r ce2297415b54 -r 6e1f3d609a68 src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Sat May 08 17:10:27 2010 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Sat May 08 16:53:53 2010 +0200 @@ -244,7 +244,7 @@ fun elim_defs thy r defs prf = let val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs - val defnames = map Thm.get_name defs; + val defnames = map Thm.derivation_name defs; val f = if not r then I else let val cnames = map (fst o dest_Const o fst) defs'; diff -r ce2297415b54 -r 6e1f3d609a68 src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Sat May 08 17:10:27 2010 +0200 +++ b/src/Pure/Thy/thm_deps.ML Sat May 08 16:53:53 2010 +0200 @@ -53,7 +53,7 @@ else let val {concealed, group, ...} = Name_Space.the_entry space name in fold_rev (fn th => - (case Thm.get_name th of + (case Thm.derivation_name th of "" => I | a => cons (a, (th, concealed, group)))) ths end; diff -r ce2297415b54 -r 6e1f3d609a68 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Sat May 08 17:10:27 2010 +0200 +++ b/src/Pure/more_thm.ML Sat May 08 16:53:53 2010 +0200 @@ -326,7 +326,7 @@ (* close_derivation *) fun close_derivation thm = - if Thm.get_name thm = "" then Thm.put_name "" thm + if Thm.derivation_name thm = "" then Thm.name_derivation "" thm else thm; diff -r ce2297415b54 -r 6e1f3d609a68 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Sat May 08 17:10:27 2010 +0200 +++ b/src/Pure/pure_thy.ML Sat May 08 16:53:53 2010 +0200 @@ -121,7 +121,7 @@ | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs; fun name_thm pre official name thm = thm - |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name) + |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name); fun name_thms pre official name xs = diff -r ce2297415b54 -r 6e1f3d609a68 src/Pure/thm.ML --- a/src/Pure/thm.ML Sat May 08 17:10:27 2010 +0200 +++ b/src/Pure/thm.ML Sat May 08 16:53:53 2010 +0200 @@ -126,8 +126,8 @@ val proof_of: thm -> proof val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool} val future: thm future -> cterm -> thm - val get_name: thm -> string - val put_name: string -> thm -> thm + val derivation_name: thm -> string + val name_derivation: string -> thm -> thm val axiom: theory -> string -> thm val axioms_of: theory -> (string * thm) list val get_tags: thm -> Properties.T @@ -585,10 +585,10 @@ (* closed derivations with official name *) -fun get_name thm = +fun derivation_name thm = Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm)); -fun put_name name (thm as Thm (der, args)) = +fun name_derivation name (thm as Thm (der, args)) = let val Deriv {promises, body} = der; val {thy_ref, hyps, prop, tpairs, ...} = args;