src/ZF/ex/Rmap.ML

--- a/src/ZF/ex/Rmap.ML	Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/Rmap.ML	Fri Jul 15 13:34:31 1994 +0200
@@ -8,6 +8,7 @@
 
 structure Rmap = Inductive_Fun
  (val thy = List.thy |> add_consts [("rmap","i=>i",NoSyn)];
+  val thy_name = "Rmap";
   val rec_doms = [("rmap", "list(domain(r))*list(range(r))")];
   val sintrs = 
       ["<Nil,Nil> : rmap(r)",