# HG changeset patch
# User wenzelm
# Date 1004133914 -7200
# Node ID f1657e0291cad1e070d4d3aade7d63c4d77d90c9
# Parent  b814360b0267d2286336eb32b2c23e5144e09230
hardwire qualified const names;

diff -r b814360b0267 -r f1657e0291ca src/HOL/Tools/datatype_abs_proofs.ML
--- 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))));
diff -r b814360b0267 -r f1657e0291ca src/HOL/Tools/datatype_prop.ML
--- 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))));
diff -r b814360b0267 -r f1657e0291ca src/HOL/Tools/datatype_rep_proofs.ML
--- 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,