Datatype: qual-ids stop creation of recursive type

Closes #257

doc/next-release.md

@@ -31,6 +31,14 @@ Bugs fixed:
 
 - `Holmake` will now follow `INCLUDES` specifications from `Holmakefiles` when given “phony” targets to build on the command-line.  (A typical phony target is `all`.) As in the past, it will still act only locally if given just a clean target (`clean`, `cleanDeps` or `cleanAll`).  To clean recursively, you must also pass the `-r` flag to `Holmake`.  ([Github issue](http://github.com/HOL-Theorem-Prover/HOL/issues/145))
 
+- `Datatype` will no longer create a recursive type if the recursive instance  is qualified with a theory name other than the current one.
+In other words,
+
+           Datatype`num = C1 num$num | C2`
+
+    won’t create a recursive type (assuming this is not called in theory `num`).
+    Thanks to Ramana Kumar for the [bug report](http://github.com/HOL-Theorem-Prover/HOL/issues/257).
+
 New theories:
 -------------
 

src/datatype/Datatype.sml

@@ -244,7 +244,8 @@ fun to_tyspecs ASTs =
      fun mk_hol_ty (dAQ ty) = ty
        | mk_hol_ty (dVartype s) = mk_vartype s
        | mk_hol_ty (dTyop{Tyop=s, Args, Thy}) =
-            if Lib.mem s new_type_names
+            if Lib.mem s new_type_names andalso
+               (Thy = NONE orelse Thy = SOME (current_theory()))
             then if null Args then tyname_as_tyvar s
                  else raise ERR "to_tyspecs"
                      ("Omit arguments to new type:"^Lib.quote s)

src/datatype/selftest.sml

@@ -253,4 +253,14 @@ val _ = Defn.Hol_defn "foo"`
 (foo2 (INL f) = INL (foo1 f))` handle HOL_ERR _ => die "FAILED!"
 val _ = print "OK\n"
 
+val _ = tprint "Non-recursive num"
+val _ = Datatype.Datatype `num = C10 num$num | C11 num | C12 scratch$num`;
+val (d,r) = dom_rng (type_of ``C10``)
+val _ = Type.compare(d, numSyntax.num) = EQUAL orelse die "FAILED!"
+val (d,r) = dom_rng (type_of ``C11``)
+val _ = Type.compare(d, numSyntax.num) <> EQUAL orelse die "FAILED!"
+val (d,r) = dom_rng (type_of ``C12``)
+val _ = Type.compare(d, numSyntax.num) <> EQUAL orelse die "FAILED!"
+val _ = print "OK\n"
+
 val _ = Process.exit Process.success;