hardwire qualified const names;

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sat Oct 27 00:00:55 2001 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Oct 27 00:05:14 2001 +0200
@@ -99,7 +99,7 @@
   let
     val _ = message "Constructing primrec combinators ...";
 
-    val fun_rel_comp_name = Sign.intern_const (sign_of Relation.thy) "fun_rel_comp";
+    val fun_rel_comp_name = "Relation.fun_rel_comp";
     val [fun_rel_comp_def, o_def] =
       map (get_thm Relation.thy) ["fun_rel_comp_def", "o_def"];
 
@@ -417,7 +417,7 @@
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
 
-    val size_name = Sign.intern_const (Theory.sign_of (theory "NatArith")) "size";
+    val size_name = "Nat.size";
     val size_names = replicate (length (hd descr)) size_name @
       map (Sign.full_name (Theory.sign_of thy1)) (DatatypeProp.indexify_names
         (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));

--- a/src/HOL/Tools/datatype_prop.ML	Sat Oct 27 00:00:55 2001 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Sat Oct 27 00:05:14 2001 +0200
@@ -168,7 +168,7 @@
 
 fun make_primrecs new_type_names descr sorts thy =
   let
-    val o_name = Sign.intern_const (sign_of Fun.thy) "op o";
+    val o_name = "Fun.op o";
 
     val sign = Theory.sign_of thy;
 
@@ -399,7 +399,7 @@
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
 
-    val size_name = Sign.intern_const (Theory.sign_of (theory "NatArith")) "size";
+    val size_name = "Nat.size";
     val size_names = replicate (length (hd descr)) size_name @
       map (Sign.intern_const (Theory.sign_of thy)) (indexify_names
         (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));

--- a/src/HOL/Tools/datatype_rep_proofs.ML	Sat Oct 27 00:00:55 2001 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sat Oct 27 00:05:14 2001 +0200
@@ -45,11 +45,16 @@
       new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
   let
     val Datatype_thy = theory "Datatype";
-    val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
-    val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name, Lim_name,
-      Funs_name, o_name, sum_case_name] =
-      map (Sign.intern_const (Theory.sign_of Datatype_thy))
-        ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o", "sum_case"];
+    val node_name = "Datatype_Universe.node";
+    val In0_name = "Datatype_Universe.In0";
+    val In1_name = "Datatype_Universe.In1";
+    val Scons_name = "Datatype_Universe.Scons";
+    val Leaf_name = "Datatype_Universe.Leaf";
+    val Numb_name = "Datatype_Universe.Numb";
+    val Lim_name = "Datatype_Universe.Lim";
+    val Funs_name = "Datatype_Universe.Funs";
+    val o_name = "Fun.op o";
+    val sum_case_name = "Datatype.sum.sum_case";
 
     val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
          In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject,