# HG changeset patch
# User wenzelm
# Date 1117533193 -7200
# Node ID 864fda4a40565b4ba58506d20a3a69300999e92a
# Parent  a80aa66d2271d4e7de3b952d2f20499cb2125413
renamed cond_extern to extern;

diff -r a80aa66d2271 -r 864fda4a4056 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Tue May 31 11:53:12 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue May 31 11:53:13 2005 +0200
@@ -99,7 +99,7 @@
 
   fun print sg tab =
     Pretty.writeln (Pretty.strs ("datatypes:" ::
-      map #1 (Sign.cond_extern_table sg Sign.typeK tab)));
+      map #1 (Sign.extern_table sg Sign.typeK tab)));
 end;
 
 structure DatatypesData = TheoryDataFun(DatatypesArgs);
@@ -466,7 +466,7 @@
         (loose_bnos (strip_abs_body t))
       end;
     val cases = map (fn ((cname, dts), t) =>
-      (Sign.cond_extern sg Sign.constK cname,
+      (Sign.extern sg Sign.constK cname,
        strip_abs (length dts) t, is_dependent (length dts) t))
       (constrs ~~ fs);
     fun count_cases (cs, (_, _, true)) = cs
diff -r a80aa66d2271 -r 864fda4a4056 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue May 31 11:53:12 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue May 31 11:53:13 2005 +0200
@@ -101,7 +101,7 @@
     (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
 
   fun print sg (tab, monos) =
-    [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
+    [Pretty.strs ("(co)inductives:" :: map #1 (Sign.extern_table sg Sign.constK tab)),
      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
     |> Pretty.chunks |> Pretty.writeln;
 end;
diff -r a80aa66d2271 -r 864fda4a4056 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Tue May 31 11:53:12 2005 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Tue May 31 11:53:13 2005 +0200
@@ -120,7 +120,7 @@
           Drule.merge_rules (wfs1, wfs2)));
 
   fun print sg (tab, hints) =
-   (Pretty.strs ("recdefs:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)) ::
+   (Pretty.strs ("recdefs:" :: map #1 (Sign.extern_table sg Sign.constK tab)) ::
      pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
 end;
 
diff -r a80aa66d2271 -r 864fda4a4056 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue May 31 11:53:12 2005 +0200
+++ b/src/Pure/axclass.ML	Tue May 31 11:53:13 2005 +0200
@@ -131,8 +131,8 @@
 
   fun print sg tab =
     let
-      val ext_class = Sign.cond_extern sg Sign.classK;
-      val ext_thm = PureThy.cond_extern_thm_sg sg;
+      val ext_class = Sign.extern sg Sign.classK;
+      val ext_thm = PureThy.extern_thm_sg sg;
 
       fun pretty_class c cs = Pretty.block
         (Pretty.str (ext_class c) :: Pretty.str " <" :: Pretty.brk 1 ::
diff -r a80aa66d2271 -r 864fda4a4056 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue May 31 11:53:12 2005 +0200
+++ b/src/Pure/codegen.ML	Tue May 31 11:53:13 2005 +0200
@@ -342,11 +342,11 @@
   end;
 
 fun mk_const_id sg s =
-  let val s' = mk_id (Sign.cond_extern sg Sign.constK s)
+  let val s' = mk_id (Sign.extern sg Sign.constK s)
   in if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' end;
 
 fun mk_type_id sg s =
-  let val s' = mk_id (Sign.cond_extern sg Sign.typeK s)
+  let val s' = mk_id (Sign.extern sg Sign.typeK s)
   in if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' end;
 
 fun rename_terms ts =
diff -r a80aa66d2271 -r 864fda4a4056 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Tue May 31 11:53:12 2005 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Tue May 31 11:53:13 2005 +0200
@@ -42,7 +42,7 @@
 
   fun print sg tab =
     Pretty.writeln (Pretty.strs ("datatypes:" ::
-      map #1 (Sign.cond_extern_table sg Sign.typeK tab)));
+      map #1 (Sign.extern_table sg Sign.typeK tab)));
   end;
 
 structure DatatypesData = TheoryDataFun(DatatypesArgs);