src/Pure/pure_thy.ML

--- a/src/Pure/pure_thy.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/pure_thy.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -83,7 +83,6 @@
 
   val empty = mk_empty ();
   fun copy (ref x) = ref x;
-  val finish = I;
   val prep_ext = mk_empty;
   val merge = mk_empty;
 
@@ -390,7 +389,6 @@
 
   val empty = {name = "", version = 0};
   val copy = I;
-  val finish = I;
   val prep_ext  = I;
   fun merge _ = empty;
   fun print _ _ = ();
@@ -424,7 +422,6 @@
 
 fun end_theory thy =
   thy
-  |> Theory.finish
   |> Theory.add_name (get_name thy);
 
 fun checkpoint thy =