# HG changeset patch
# User wenzelm
# Date 1506717809 -7200
# Node ID 9c661b74ce9230b17e4379242b49fca76d320290
# Parent  ae38b8c0fdd9c46bdd1cf366080ceef238f114f6
unused;

diff -r ae38b8c0fdd9 -r 9c661b74ce92 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Sep 29 22:41:19 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 22:43:29 2017 +0200
@@ -102,8 +102,6 @@
 
   object Base
   {
-    def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
-
     def bootstrap(global_theories: Map[String, String]): Base =
       Base(
         global_theories = global_theories,