# HG changeset patch
# User wenzelm
# Date 911209566 -3600
# Node ID 6aae55ae3473c20447081fbed9917cefb22e2cf8
# Parent  a58d4528121dc2006ef62b8d6e7130168fa38b4e
renamed init_context to init;

diff -r a58d4528121d -r 6aae55ae3473 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Nov 16 10:45:52 1998 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Nov 16 10:46:06 1998 +0100
@@ -137,7 +137,7 @@
   State (make_node (f (context, facts, mode, goal)), nodes);
 
 fun init_state thy =
-  State (make_node (ProofContext.init_context thy, None, Forward, None), []);
+  State (make_node (ProofContext.init thy, None, Forward, None), []);