# HG changeset patch
# User wenzelm
# Date 879777625 -3600
# Node ID c4f1d3940d9599175425277942c75f75d2c9828e
# Parent  59af75feccc424fb1192c3ce885ae0af31f7e405
improved big_rec_name lookup;

diff -r 59af75feccc4 -r c4f1d3940d95 src/HOL/add_ind_def.ML
--- 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);
diff -r 59af75feccc4 -r c4f1d3940d95 src/ZF/add_ind_def.ML
--- 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);