# HG changeset patch
# User wenzelm
# Date 1216027176 -7200
# Node ID 14b238b1000c3305f5416f696eec9cdf54395c2a
# Parent  33f215fa079e3685b1f6d9efd20aeebd2a67fe8b
removed Isar/proof_history.ML;
added Isar/proof_node.ML

diff -r 33f215fa079e -r 14b238b1000c src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Mon Jul 14 11:04:47 2008 +0200
+++ b/src/Pure/IsaMakefile	Mon Jul 14 11:19:36 2008 +0200
@@ -41,7 +41,7 @@
   Isar/obtain.ML Isar/outer_keyword.ML Isar/outer_lex.ML		\
   Isar/outer_parse.ML Isar/outer_syntax.ML Isar/overloading.ML		\
   Isar/proof.ML Isar/proof_context.ML Isar/proof_display.ML		\
-  Isar/proof_history.ML Isar/rule_cases.ML Isar/rule_insts.ML		\
+  Isar/proof_node.ML Isar/rule_cases.ML Isar/rule_insts.ML		\
   Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML			\
   Isar/specification.ML Isar/subclass.ML Isar/theory_target.ML		\
   Isar/toplevel.ML ML-Systems/alice.ML ML-Systems/exn.ML		\
diff -r 33f215fa079e -r 14b238b1000c src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Mon Jul 14 11:04:47 2008 +0200
+++ b/src/Pure/Isar/ROOT.ML	Mon Jul 14 11:19:36 2008 +0200
@@ -69,7 +69,7 @@
 use "constdefs.ML";
 
 (*toplevel transactions*)
-use "proof_history.ML";
+use "proof_node.ML";
 use "toplevel.ML";
 
 (*theory syntax*)