improved big_rec_name lookup;

--- a/src/HOL/add_ind_def.ML	Mon Nov 17 10:50:03 1997 +0100
+++ b/src/HOL/add_ind_def.ML	Mon Nov 17 15:40:25 1997 +0100
@@ -138,7 +138,7 @@
       If no mutual recursion then it equals the one recursive set.
       If mutual recursion then it differs from all the recursive sets. *)
     val big_rec_base_name = space_implode "_" rec_base_names;
-    val big_rec_name = Sign.full_name sign big_rec_base_name;
+    val big_rec_name = Sign.intern_const sign big_rec_base_name;
 
     (*Big_rec... is the union of the mutually recursive sets*)
     val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);

--- a/src/ZF/add_ind_def.ML	Mon Nov 17 10:50:03 1997 +0100
+++ b/src/ZF/add_ind_def.ML	Mon Nov 17 15:40:25 1997 +0100
@@ -149,7 +149,7 @@
       If no mutual recursion then it equals the one recursive set.
       If mutual recursion then it differs from all the recursive sets. *)
     val big_rec_base_name = space_implode "_" rec_base_names;
-    val big_rec_name = Sign.full_name sign big_rec_base_name;
+    val big_rec_name = Sign.intern_const sign big_rec_base_name;
 
     (*Big_rec... is the union of the mutually recursive sets*)
     val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);