do not export Attrib.register_config, to make it harder to use low-level Config.declare after the bootstrap phase;
authorwenzelm
Sun Mar 28 15:38:07 2010 +0200 (2010-03-28 ago)
changeset 359986b8f789554ae
parent 35997 07bce2802939
child 35999 e031755609cf
do not export Attrib.register_config, to make it harder to use low-level Config.declare after the bootstrap phase;
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Sun Mar 28 15:13:19 2010 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun Mar 28 15:38:07 2010 +0200
     1.3 @@ -36,7 +36,6 @@
     1.4    val multi_thm: thm list context_parser
     1.5    val print_configs: Proof.context -> unit
     1.6    val internal: (morphism -> attribute) -> src
     1.7 -  val register_config: Config.value Config.T -> theory -> theory
     1.8    val config_bool: bstring -> bool -> bool Config.T * (theory -> theory)
     1.9    val config_int: bstring -> int -> int Config.T * (theory -> theory)
    1.10    val config_string: bstring -> string -> string Config.T * (theory -> theory)