src/HOL/Tools/datatype_prop.ML
changeset 11957 f1657e0291ca
parent 11539 0f17da240450
child 12338 de0f4a63baa5
--- 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))));