# HG changeset patch # User wenzelm # Date 1269783487 -7200 # Node ID 6b8f789554ae9423bb001640d564178c107ee81b # Parent 07bce2802939b4c167878fc1af3497d7e1164ed7 do not export Attrib.register_config, to make it harder to use low-level Config.declare after the bootstrap phase; diff -r 07bce2802939 -r 6b8f789554ae src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Sun Mar 28 15:13:19 2010 +0200 +++ b/src/Pure/Isar/attrib.ML Sun Mar 28 15:38:07 2010 +0200 @@ -36,7 +36,6 @@ val multi_thm: thm list context_parser val print_configs: Proof.context -> unit val internal: (morphism -> attribute) -> src - val register_config: Config.value Config.T -> theory -> theory val config_bool: bstring -> bool -> bool Config.T * (theory -> theory) val config_int: bstring -> int -> int Config.T * (theory -> theory) val config_string: bstring -> string -> string Config.T * (theory -> theory)