renamed cond_extern to extern;
authorwenzelm
Tue May 31 11:53:13 2005 +0200 (2005-05-31 ago)
changeset 16122864fda4a4056
parent 16121 a80aa66d2271
child 16123 1381e90c2694
renamed cond_extern to extern;
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/recdef_package.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/ZF/Tools/induct_tacs.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue May 31 11:53:12 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue May 31 11:53:13 2005 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4  
     1.5    fun print sg tab =
     1.6      Pretty.writeln (Pretty.strs ("datatypes:" ::
     1.7 -      map #1 (Sign.cond_extern_table sg Sign.typeK tab)));
     1.8 +      map #1 (Sign.extern_table sg Sign.typeK tab)));
     1.9  end;
    1.10  
    1.11  structure DatatypesData = TheoryDataFun(DatatypesArgs);
    1.12 @@ -466,7 +466,7 @@
    1.13          (loose_bnos (strip_abs_body t))
    1.14        end;
    1.15      val cases = map (fn ((cname, dts), t) =>
    1.16 -      (Sign.cond_extern sg Sign.constK cname,
    1.17 +      (Sign.extern sg Sign.constK cname,
    1.18         strip_abs (length dts) t, is_dependent (length dts) t))
    1.19        (constrs ~~ fs);
    1.20      fun count_cases (cs, (_, _, true)) = cs
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Tue May 31 11:53:12 2005 +0200
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue May 31 11:53:13 2005 +0200
     2.3 @@ -101,7 +101,7 @@
     2.4      (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
     2.5  
     2.6    fun print sg (tab, monos) =
     2.7 -    [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
     2.8 +    [Pretty.strs ("(co)inductives:" :: map #1 (Sign.extern_table sg Sign.constK tab)),
     2.9       Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
    2.10      |> Pretty.chunks |> Pretty.writeln;
    2.11  end;
     3.1 --- a/src/HOL/Tools/recdef_package.ML	Tue May 31 11:53:12 2005 +0200
     3.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue May 31 11:53:13 2005 +0200
     3.3 @@ -120,7 +120,7 @@
     3.4            Drule.merge_rules (wfs1, wfs2)));
     3.5  
     3.6    fun print sg (tab, hints) =
     3.7 -   (Pretty.strs ("recdefs:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)) ::
     3.8 +   (Pretty.strs ("recdefs:" :: map #1 (Sign.extern_table sg Sign.constK tab)) ::
     3.9       pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
    3.10  end;
    3.11  
     4.1 --- a/src/Pure/axclass.ML	Tue May 31 11:53:12 2005 +0200
     4.2 +++ b/src/Pure/axclass.ML	Tue May 31 11:53:13 2005 +0200
     4.3 @@ -131,8 +131,8 @@
     4.4  
     4.5    fun print sg tab =
     4.6      let
     4.7 -      val ext_class = Sign.cond_extern sg Sign.classK;
     4.8 -      val ext_thm = PureThy.cond_extern_thm_sg sg;
     4.9 +      val ext_class = Sign.extern sg Sign.classK;
    4.10 +      val ext_thm = PureThy.extern_thm_sg sg;
    4.11  
    4.12        fun pretty_class c cs = Pretty.block
    4.13          (Pretty.str (ext_class c) :: Pretty.str " <" :: Pretty.brk 1 ::
     5.1 --- a/src/Pure/codegen.ML	Tue May 31 11:53:12 2005 +0200
     5.2 +++ b/src/Pure/codegen.ML	Tue May 31 11:53:13 2005 +0200
     5.3 @@ -342,11 +342,11 @@
     5.4    end;
     5.5  
     5.6  fun mk_const_id sg s =
     5.7 -  let val s' = mk_id (Sign.cond_extern sg Sign.constK s)
     5.8 +  let val s' = mk_id (Sign.extern sg Sign.constK s)
     5.9    in if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' end;
    5.10  
    5.11  fun mk_type_id sg s =
    5.12 -  let val s' = mk_id (Sign.cond_extern sg Sign.typeK s)
    5.13 +  let val s' = mk_id (Sign.extern sg Sign.typeK s)
    5.14    in if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' end;
    5.15  
    5.16  fun rename_terms ts =
     6.1 --- a/src/ZF/Tools/induct_tacs.ML	Tue May 31 11:53:12 2005 +0200
     6.2 +++ b/src/ZF/Tools/induct_tacs.ML	Tue May 31 11:53:13 2005 +0200
     6.3 @@ -42,7 +42,7 @@
     6.4  
     6.5    fun print sg tab =
     6.6      Pretty.writeln (Pretty.strs ("datatypes:" ::
     6.7 -      map #1 (Sign.cond_extern_table sg Sign.typeK tab)));
     6.8 +      map #1 (Sign.extern_table sg Sign.typeK tab)));
     6.9    end;
    6.10  
    6.11  structure DatatypesData = TheoryDataFun(DatatypesArgs);