src/Pure/thm.ML
changeset 4018 09b77900af0f
parent 3994 0343230ec85c
child 4036 bd686e39bff8
     1.1 --- a/src/Pure/thm.ML	Tue Oct 28 17:29:48 1997 +0100
     1.2 +++ b/src/Pure/thm.ML	Tue Oct 28 17:30:47 1997 +0100
     1.3 @@ -100,6 +100,7 @@
     1.4    val implies_intr_shyps: thm -> thm
     1.5    val get_axiom         : theory -> xstring -> thm
     1.6    val name_thm          : string * thm -> thm
     1.7 +  val name_of_thm	: thm -> string
     1.8    val axioms_of         : theory -> (string * thm) list
     1.9  
    1.10    (*meta rules*)
    1.11 @@ -603,13 +604,18 @@
    1.12      (Symtab.dest (#axioms (rep_theory thy)));
    1.13  
    1.14  (*Attach a label to a theorem to make proof objects more readable*)
    1.15 -fun name_thm (name, th as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 
    1.16 -    Thm {sign_ref = sign_ref, 
    1.17 -         der = Join (Theorem name, [der]),
    1.18 -         maxidx = maxidx,
    1.19 -         shyps = shyps, 
    1.20 -         hyps = hyps, 
    1.21 -         prop = prop};
    1.22 +fun name_thm (name, th as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
    1.23 +  (case der of
    1.24 +    Join (Theorem _, _) => th
    1.25 +  | Join (Axiom _, _) => th
    1.26 +  | _ => Thm {sign_ref = sign_ref, der = Join (Theorem name, [der]),
    1.27 +      maxidx = maxidx, shyps = shyps, hyps = hyps, prop = prop});
    1.28 +
    1.29 +fun name_of_thm (Thm {der, ...}) =
    1.30 +  (case der of
    1.31 +    Join (Theorem name, _) => name
    1.32 +  | Join (Axiom (_, name), _) => name
    1.33 +  | _ => "");
    1.34  
    1.35  
    1.36  (*Compression of theorems -- a separate rule, not integrated with the others,