src/Pure/Isar/isar_cmd.ML
changeset 56005 4f4fc80b0613
parent 55828 42ac3cfb89f6
child 56006 6a4dcaf53664
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Mar 09 17:07:45 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 09 17:08:31 2014 +0100
     1.3 @@ -21,10 +21,6 @@
     1.4      Symbol_Pos.source -> local_theory -> local_theory
     1.5    val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source ->
     1.6      string list -> local_theory -> local_theory
     1.7 -  val hide_class: bool -> xstring list -> theory -> theory
     1.8 -  val hide_type: bool -> xstring list -> theory -> theory
     1.9 -  val hide_const: bool -> xstring list -> theory -> theory
    1.10 -  val hide_fact: bool -> xstring list -> theory -> theory
    1.11    val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    1.12    val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    1.13    val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    1.14 @@ -183,24 +179,6 @@
    1.15    |> Context.proof_map;
    1.16  
    1.17  
    1.18 -(* hide names *)
    1.19 -
    1.20 -fun hide_names intern check hide fully xnames thy =
    1.21 -  let
    1.22 -    val names = map (intern thy) xnames;
    1.23 -    val bads = filter_out (check thy) names;
    1.24 -  in
    1.25 -    if null bads then fold (hide fully) names thy
    1.26 -    else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
    1.27 -  end;
    1.28 -
    1.29 -val hide_class = hide_names Sign.intern_class (can o Sign.certify_class) Sign.hide_class;
    1.30 -val hide_type = hide_names Sign.intern_type Sign.declared_tyname Sign.hide_type;
    1.31 -val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const;
    1.32 -val hide_fact =
    1.33 -  hide_names Global_Theory.intern_fact Global_Theory.defined_fact Global_Theory.hide_fact;
    1.34 -
    1.35 -
    1.36  (* goals *)
    1.37  
    1.38  fun goal opt_chain goal stmt int =