src/ZF/ex/PropLog.ML

--- a/src/ZF/ex/PropLog.ML	Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/PropLog.ML	Fri Jul 15 13:34:31 1994 +0200
@@ -78,6 +78,7 @@
 
 structure PropThms = Inductive_Fun
  (val thy = PropLog.thy;
+  val thy_name = "PropThms";
   val rec_doms = [("thms","prop")];
   val sintrs = 
       ["[| p:H;  p:prop |] ==> H |- p",