# HG changeset patch
# User haftmann
# Date 1262697552 -3600
# Node ID 95df5e6dd41c82383039a41b63d56f6e339309e9
# Parent  70af06abb13d0334567180203c439c0e9d3b557e
avoid exporting Type.build_tsig

diff -r 70af06abb13d -r 95df5e6dd41c src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jan 05 11:38:51 2010 +0100
+++ b/src/Pure/Isar/code.ML	Tue Jan 05 14:19:12 2010 +0100
@@ -317,9 +317,14 @@
   let
     val (tycos, _) = (the_signatures o the_exec) thy;
     val decls = (#types o Type.rep_tsig o Sign.tsig_of) thy
-      |> apsnd (Symtab.fold (fn (tyco, n) =>
-          Symtab.update (tyco, Type.LogicalType n)) tycos);
-  in Type.build_tsig ((Name_Space.empty "", Sorts.empty_algebra), [], decls) end;
+      |> snd 
+      |> Symtab.fold (fn (tyco, n) =>
+          Symtab.update (tyco, Type.LogicalType n)) tycos;
+  in
+    Type.empty_tsig
+    |> Symtab.fold (fn (tyco, Type.LogicalType n) => Type.add_type Name_Space.default_naming
+        (Binding.qualified_name tyco, n) | _ => I) decls
+  end;
 
 fun cert_signature thy = Logic.varifyT o Type.cert_typ (build_tsig thy) o Type.no_tvars;
 
diff -r 70af06abb13d -r 95df5e6dd41c src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Jan 05 11:38:51 2010 +0100
+++ b/src/Pure/type.ML	Tue Jan 05 14:19:12 2010 +0100
@@ -19,7 +19,6 @@
     types: decl Name_Space.table,
     log_types: string list}
   val empty_tsig: tsig
-  val build_tsig: (Name_Space.T * Sorts.algebra) * sort * decl Name_Space.table -> tsig
   val defaultS: tsig -> sort
   val logical_types: tsig -> string list
   val eq_sort: tsig -> sort * sort -> bool