Thm.proof_of;
authorwenzelm
Tue Aug 27 11:06:20 2002 +0200 (2002-08-27)
changeset 135304813fdc0ef17
parent 13529 49a0ad8f175e
child 13531 5825aef91ac5
Thm.proof_of;
src/Pure/Proof/proof_syntax.ML
src/Pure/Thy/thm_deps.ML
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Aug 27 11:06:07 2002 +0200
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Aug 27 11:06:20 2002 +0200
     1.3 @@ -147,7 +147,7 @@
     1.4               | "thm" :: xs =>
     1.5                   let val name = NameSpace.pack xs;
     1.6                   in (case assoc (thms, name) of
     1.7 -                     Some thm => fst (strip_combt (#2 (#der (rep_thm thm))))
     1.8 +                     Some thm => fst (strip_combt (Thm.proof_of thm))
     1.9                     | None => (case Symtab.lookup (tab, name) of
    1.10                           Some prf => prf
    1.11                         | None => error ("Unknown theorem " ^ quote name)))
     2.1 --- a/src/Pure/Thy/thm_deps.ML	Tue Aug 27 11:06:07 2002 +0200
     2.2 +++ b/src/Pure/Thy/thm_deps.ML	Tue Aug 27 11:06:20 2002 +0200
     2.3 @@ -70,7 +70,7 @@
     2.4    let
     2.5      val _ = writeln "Generating graph ...";
     2.6      val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
     2.7 -      map (#2 o #der o Thm.rep_thm) thms))));
     2.8 +      map Thm.proof_of thms))));
     2.9      val path = File.tmp_path (Path.unpack "theorems.graph");
    2.10      val _ = Present.write_graph gra path;
    2.11      val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");