src/HOL/Tools/inductive_package.ML
changeset 16122 864fda4a4056
parent 15794 5de27a5fc5ed
child 16287 7a03b4b4df67
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue May 31 11:53:12 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue May 31 11:53:13 2005 +0200
     1.3 @@ -101,7 +101,7 @@
     1.4      (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
     1.5  
     1.6    fun print sg (tab, monos) =
     1.7 -    [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
     1.8 +    [Pretty.strs ("(co)inductives:" :: map #1 (Sign.extern_table sg Sign.constK tab)),
     1.9       Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
    1.10      |> Pretty.chunks |> Pretty.writeln;
    1.11  end;