# HG changeset patch
# User paulson
# Date 827402987 -3600
# Node ID 6f4d995590fd14561d0615f845f91c637938c61d
# Parent 54ece585bf622827445daa0f38c3ee29c1d2c5b3
For the new version of name_thm. Now the same theorem
is stored as is returned, as both contain a label and a link to the
previous derivation. So get_thm no longer needs to attach a label to
its resulting theorem.
diff -r 54ece585bf62 -r 6f4d995590fd src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML Thu Mar 21 11:06:59 1996 +0100
+++ b/src/Pure/Thy/thy_read.ML Thu Mar 21 11:09:47 1996 +0100
@@ -1073,8 +1073,8 @@
| None => ()
end;
- (*Return version with trivial proof object; store original version *)
- val thm' = Thm.name_thm (the theory, name, thm) handle OPTION _ => thm
+ (*Label this theorem*)
+ val thm' = Thm.name_thm (name, thm)
in
loaded_thys := Symtab.update
((thy_name, ThyInfo {path = path, children = children, parents = parents,
@@ -1118,8 +1118,7 @@
let val ThyInfo {thms, ...} = the (get_thyinfo name);
in thms end;
-(*Get a stored theorem specified by theory and name.
- Derivation has the form Theorem(thy,name). *)
+(*Get a stored theorem specified by theory and name. *)
fun get_thm thy name =
let fun get [] [] searched =
raise THEORY ("get_thm: no theorem " ^ quote name, [thy])
@@ -1127,7 +1126,7 @@
get (ng \\ searched) [] searched
| get (t::ts) ng searched =
(case Symtab.lookup (thmtab_of_name t, name) of
- Some thm => Thm.name_thm(thy,name,thm)
+ Some thm => thm
| None => get ts (ng union (parents_of_name t)) (t::searched));
val (tname, _) = thyinfo_of_sign (sign_of thy);
@@ -1303,7 +1302,7 @@
Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms))
end;
-fun print_theory thy = (Drule.print_theory thy; print_thms thy);
+fun print_theory thy = (Display.print_theory thy; print_thms thy);
(*** Misc functions ***)