clarified bootstrap -- more uniform use of ML files;
authorwenzelm
Mon Apr 04 17:02:34 2016 +0200 (2016-04-04)
changeset 62848e4140efe699e
parent 62847 1bd1d8492931
child 62849 caaa2fc4040d
clarified bootstrap -- more uniform use of ML files;
src/Pure/Isar/calculation.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Tools/class_deps.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/named_theorems.ML
src/Pure/Tools/thm_deps.ML
src/Pure/Tools/thy_deps.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Mon Apr 04 16:14:22 2016 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Mon Apr 04 17:02:34 2016 +0200
     1.3 @@ -205,32 +205,4 @@
     1.4  val moreover = collect false;
     1.5  val ultimately = collect true;
     1.6  
     1.7 -
     1.8 -(* outer syntax *)
     1.9 -
    1.10 -val calc_args =
    1.11 -  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
    1.12 -
    1.13 -val _ =
    1.14 -  Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
    1.15 -    (calc_args >> (Toplevel.proofs' o also_cmd));
    1.16 -
    1.17 -val _ =
    1.18 -  Outer_Syntax.command @{command_keyword finally}
    1.19 -    "combine calculation and current facts, exhibit result"
    1.20 -    (calc_args >> (Toplevel.proofs' o finally_cmd));
    1.21 -
    1.22 -val _ =
    1.23 -  Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts"
    1.24 -    (Scan.succeed (Toplevel.proof' moreover));
    1.25 -
    1.26 -val _ =
    1.27 -  Outer_Syntax.command @{command_keyword ultimately}
    1.28 -    "augment calculation by current facts, exhibit result"
    1.29 -    (Scan.succeed (Toplevel.proof' ultimately));
    1.30 -
    1.31 -val _ =
    1.32 -  Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
    1.33 -    (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of)));
    1.34 -
    1.35  end;
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Apr 04 16:14:22 2016 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Apr 04 17:02:34 2016 +0200
     2.3 @@ -148,6 +148,12 @@
     2.4        >> (fn (facts, fixes) =>
     2.5            #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
     2.6  
     2.7 +val _ =
     2.8 +  Outer_Syntax.local_theory @{command_keyword named_theorems}
     2.9 +    "declare named collection of theorems"
    2.10 +    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
    2.11 +      fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
    2.12 +
    2.13  
    2.14  (* hide names *)
    2.15  
    2.16 @@ -728,6 +734,34 @@
    2.17  end;
    2.18  
    2.19  
    2.20 +(* calculation *)
    2.21 +
    2.22 +val calculation_args =
    2.23 +  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
    2.24 +
    2.25 +val _ =
    2.26 +  Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
    2.27 +    (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd));
    2.28 +
    2.29 +val _ =
    2.30 +  Outer_Syntax.command @{command_keyword finally}
    2.31 +    "combine calculation and current facts, exhibit result"
    2.32 +    (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd));
    2.33 +
    2.34 +val _ =
    2.35 +  Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts"
    2.36 +    (Scan.succeed (Toplevel.proof' Calculation.moreover));
    2.37 +
    2.38 +val _ =
    2.39 +  Outer_Syntax.command @{command_keyword ultimately}
    2.40 +    "augment calculation by current facts, exhibit result"
    2.41 +    (Scan.succeed (Toplevel.proof' Calculation.ultimately));
    2.42 +
    2.43 +val _ =
    2.44 +  Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
    2.45 +    (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
    2.46 +
    2.47 +
    2.48  (* proof navigation *)
    2.49  
    2.50  fun report_back () =
    2.51 @@ -936,6 +970,96 @@
    2.52        Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
    2.53  
    2.54  
    2.55 +(* deps *)
    2.56 +
    2.57 +local
    2.58 +  val theory_bounds =
    2.59 +    Parse.position Parse.theory_xname >> single ||
    2.60 +    (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
    2.61 +in
    2.62 +
    2.63 +val _ =
    2.64 +  Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
    2.65 +    (Scan.option theory_bounds -- Scan.option theory_bounds >>
    2.66 +      (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args)));
    2.67 +
    2.68 +end;
    2.69 +
    2.70 +local
    2.71 +  val class_bounds =
    2.72 +    Parse.sort >> single ||
    2.73 +    (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
    2.74 +in
    2.75 +
    2.76 +val _ =
    2.77 +  Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
    2.78 +    (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
    2.79 +      Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args)));
    2.80 +
    2.81 +end;
    2.82 +
    2.83 +val _ =
    2.84 +  Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
    2.85 +    (Parse.xthms1 >> (fn args =>
    2.86 +      Toplevel.keep (fn st =>
    2.87 +        Thm_Deps.thm_deps (Toplevel.theory_of st)
    2.88 +          (Attrib.eval_thms (Toplevel.context_of st) args))));
    2.89 +
    2.90 +local
    2.91 +  val thy_names =
    2.92 +    Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
    2.93 +in
    2.94 +
    2.95 +val _ =
    2.96 +  Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
    2.97 +    (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
    2.98 +        Toplevel.keep (fn st =>
    2.99 +          let
   2.100 +            val thy = Toplevel.theory_of st;
   2.101 +            val ctxt = Toplevel.context_of st;
   2.102 +            fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
   2.103 +            val check = Theory.check ctxt;
   2.104 +          in
   2.105 +            Thm_Deps.unused_thms
   2.106 +              (case opt_range of
   2.107 +                NONE => (Theory.parents_of thy, [thy])
   2.108 +              | SOME (xs, NONE) => (map check xs, [thy])
   2.109 +              | SOME (xs, SOME ys) => (map check xs, map check ys))
   2.110 +            |> map pretty_thm |> Pretty.writeln_chunks
   2.111 +          end)));
   2.112 +
   2.113 +end;
   2.114 +
   2.115 +
   2.116 +(* find *)
   2.117 +
   2.118 +val _ =
   2.119 +  Outer_Syntax.command @{command_keyword find_consts}
   2.120 +    "find constants by name / type patterns"
   2.121 +    (Find_Consts.query_parser >> (fn spec =>
   2.122 +      Toplevel.keep (fn st =>
   2.123 +        Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec))));
   2.124 +
   2.125 +local
   2.126 +  val options =
   2.127 +    Scan.optional
   2.128 +      (Parse.$$$ "(" |--
   2.129 +        Parse.!!! (Scan.option Parse.nat --
   2.130 +          Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
   2.131 +      (NONE, true);
   2.132 +in
   2.133 +
   2.134 +val _ =
   2.135 +  Outer_Syntax.command @{command_keyword find_theorems}
   2.136 +    "find theorems meeting specified criteria"
   2.137 +    (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) =>
   2.138 +      Toplevel.keep (fn st =>
   2.139 +        Pretty.writeln
   2.140 +          (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec))));
   2.141 +
   2.142 +end;
   2.143 +
   2.144 +
   2.145  
   2.146  (** extraction of programs from proofs **)
   2.147  
     3.1 --- a/src/Pure/Pure.thy	Mon Apr 04 16:14:22 2016 +0200
     3.2 +++ b/src/Pure/Pure.thy	Mon Apr 04 17:02:34 2016 +0200
     3.3 @@ -93,23 +93,7 @@
     3.4    and "named_theorems" :: thy_decl
     3.5  begin
     3.6  
     3.7 -ML_file "ML/ml_antiquotations.ML"
     3.8 -ML_file "ML/ml_thms.ML"
     3.9 -ML_file "Tools/print_operation.ML"
    3.10  ML_file "Isar/isar_syn.ML"
    3.11 -ML_file "Isar/calculation.ML"
    3.12 -ML_file "Tools/bibtex.ML"
    3.13 -ML_file "Tools/rail.ML"
    3.14 -ML_file "Tools/rule_insts.ML"
    3.15 -ML_file "Tools/thm_deps.ML"
    3.16 -ML_file "Tools/thy_deps.ML"
    3.17 -ML_file "Tools/class_deps.ML"
    3.18 -ML_file "Tools/find_theorems.ML"
    3.19 -ML_file "Tools/find_consts.ML"
    3.20 -ML_file "Tools/simplifier_trace.ML"
    3.21 -ML_file_no_debug "Tools/debugger.ML"
    3.22 -ML_file "Tools/named_theorems.ML"
    3.23 -ML_file "Tools/jedit.ML"
    3.24  
    3.25  
    3.26  section \<open>Basic attributes\<close>
     4.1 --- a/src/Pure/ROOT	Mon Apr 04 16:14:22 2016 +0200
     4.2 +++ b/src/Pure/ROOT	Mon Apr 04 17:02:34 2016 +0200
     4.3 @@ -61,6 +61,7 @@
     4.4      "Isar/attrib.ML"
     4.5      "Isar/auto_bind.ML"
     4.6      "Isar/bundle.ML"
     4.7 +    "Isar/calculation.ML"
     4.8      "Isar/class.ML"
     4.9      "Isar/class_declaration.ML"
    4.10      "Isar/code.ML"
    4.11 @@ -99,6 +100,7 @@
    4.12      "ML/exn_properties.ML"
    4.13      "ML/fixed_int_dummy.ML"
    4.14      "ML/ml_antiquotation.ML"
    4.15 +    "ML/ml_antiquotations.ML"
    4.16      "ML/ml_compiler.ML"
    4.17      "ML/ml_compiler0.ML"
    4.18      "ML/ml_compiler1.ML"
    4.19 @@ -112,13 +114,14 @@
    4.20      "ML/ml_lex.ML"
    4.21      "ML/ml_name_space.ML"
    4.22      "ML/ml_options.ML"
    4.23 +    "ML/ml_pervasive.ML"
    4.24      "ML/ml_pp.ML"
    4.25 -    "ML/ml_pervasive.ML"
    4.26      "ML/ml_pretty.ML"
    4.27      "ML/ml_profiling.ML"
    4.28      "ML/ml_statistics.ML"
    4.29      "ML/ml_syntax.ML"
    4.30      "ML/ml_system.ML"
    4.31 +    "ML/ml_thms.ML"
    4.32      "PIDE/active.ML"
    4.33      "PIDE/command.ML"
    4.34      "PIDE/command_span.ML"
    4.35 @@ -172,9 +175,22 @@
    4.36      "Thy/thy_info.ML"
    4.37      "Thy/thy_output.ML"
    4.38      "Thy/thy_syntax.ML"
    4.39 +    "Tools/bibtex.ML"
    4.40      "Tools/build.ML"
    4.41 +    "Tools/class_deps.ML"
    4.42 +    "Tools/debugger.ML"
    4.43 +    "Tools/find_consts.ML"
    4.44 +    "Tools/find_theorems.ML"
    4.45 +    "Tools/jedit.ML"
    4.46 +    "Tools/named_theorems.ML"
    4.47      "Tools/named_thms.ML"
    4.48      "Tools/plugin.ML"
    4.49 +    "Tools/print_operation.ML"
    4.50 +    "Tools/rail.ML"
    4.51 +    "Tools/rule_insts.ML"
    4.52 +    "Tools/simplifier_trace.ML"
    4.53 +    "Tools/thm_deps.ML"
    4.54 +    "Tools/thy_deps.ML"
    4.55      "assumption.ML"
    4.56      "axclass.ML"
    4.57      "config.ML"
     5.1 --- a/src/Pure/ROOT.ML	Mon Apr 04 16:14:22 2016 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Mon Apr 04 17:02:34 2016 +0200
     5.3 @@ -241,6 +241,7 @@
     5.4  use "Isar/element.ML";
     5.5  use "Isar/obtain.ML";
     5.6  use "Isar/subgoal.ML";
     5.7 +use "Isar/calculation.ML";
     5.8  
     5.9  (*local theories and targets*)
    5.10  use "Isar/locale.ML";
    5.11 @@ -321,6 +322,23 @@
    5.12  use "Tools/named_thms.ML";
    5.13  use "ML/ml_pp.ML";
    5.14  use "ML/ml_file.ML";
    5.15 +use "ML/ml_antiquotations.ML";
    5.16 +use "ML/ml_thms.ML";
    5.17 +use "Tools/print_operation.ML";
    5.18 +
    5.19 +use "Tools/bibtex.ML";
    5.20 +use "Tools/rail.ML";
    5.21 +use "Tools/rule_insts.ML";
    5.22 +use "Tools/thm_deps.ML";
    5.23 +use "Tools/thy_deps.ML";
    5.24 +use "Tools/class_deps.ML";
    5.25 +use "Tools/find_theorems.ML";
    5.26 +use "Tools/find_consts.ML";
    5.27 +use "Tools/simplifier_trace.ML";
    5.28 +use_no_debug "Tools/debugger.ML";
    5.29 +use "Tools/named_theorems.ML";
    5.30 +use "Tools/jedit.ML";
    5.31 +
    5.32  use_thy "Pure";
    5.33  
    5.34  
     6.1 --- a/src/Pure/Tools/class_deps.ML	Mon Apr 04 16:14:22 2016 +0200
     6.2 +++ b/src/Pure/Tools/class_deps.ML	Mon Apr 04 17:02:34 2016 +0200
     6.3 @@ -37,13 +37,4 @@
     6.4  val class_deps = gen_class_deps (Type.cert_sort o Proof_Context.tsig_of);
     6.5  val class_deps_cmd = Graph_Display.display_graph oo gen_class_deps Syntax.read_sort;
     6.6  
     6.7 -val class_bounds =
     6.8 -  Parse.sort >> single ||
     6.9 -  (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
    6.10 -
    6.11 -val _ =
    6.12 -  Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
    6.13 -    (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
    6.14 -      Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) args)));
    6.15 -
    6.16  end;
     7.1 --- a/src/Pure/Tools/find_consts.ML	Mon Apr 04 16:14:22 2016 +0200
     7.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Apr 04 17:02:34 2016 +0200
     7.3 @@ -11,6 +11,8 @@
     7.4        Strict of string
     7.5      | Loose of string
     7.6      | Name of string
     7.7 +  val pretty_consts: Proof.context -> (bool * criterion) list -> Pretty.T
     7.8 +  val query_parser: (bool * criterion) list parser
     7.9    val read_query: Position.T -> string -> (bool * criterion) list
    7.10    val find_consts : Proof.context -> (bool * criterion) list -> unit
    7.11  end;
    7.12 @@ -138,25 +140,18 @@
    7.13    Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
    7.14    Parse.typ >> Loose;
    7.15  
    7.16 -val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
    7.17 -
    7.18  val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
    7.19  
    7.20  in
    7.21  
    7.22 +val query_parser = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
    7.23 +
    7.24  fun read_query pos str =
    7.25    Token.explode query_keywords pos str
    7.26    |> filter Token.is_proper
    7.27 -  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
    7.28 +  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query_parser --| Scan.ahead Parse.eof)))
    7.29    |> #1;
    7.30  
    7.31 -val _ =
    7.32 -  Outer_Syntax.command @{command_keyword find_consts}
    7.33 -    "find constants by name / type patterns"
    7.34 -    (query >> (fn spec =>
    7.35 -      Toplevel.keep (fn st =>
    7.36 -        Pretty.writeln (pretty_consts (Toplevel.context_of st) spec))));
    7.37 -
    7.38  end;
    7.39  
    7.40  
     8.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Apr 04 16:14:22 2016 +0200
     8.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Apr 04 17:02:34 2016 +0200
     8.3 @@ -15,12 +15,16 @@
     8.4      rem_dups: bool,
     8.5      criteria: (bool * 'term criterion) list
     8.6    }
     8.7 +  val query_parser: (bool * string criterion) list parser
     8.8    val read_query: Position.T -> string -> (bool * string criterion) list
     8.9    val find_theorems: Proof.context -> thm option -> int option -> bool ->
    8.10      (bool * term criterion) list -> int option * (Facts.ref * thm) list
    8.11    val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
    8.12      (bool * string criterion) list -> int option * (Facts.ref * thm) list
    8.13    val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
    8.14 +  val pretty_theorems: Proof.state ->
    8.15 +    int option -> bool -> (bool * string criterion) list -> Pretty.T
    8.16 +  val proof_state: Toplevel.state -> Proof.state
    8.17  end;
    8.18  
    8.19  structure Find_Theorems: FIND_THEOREMS =
    8.20 @@ -502,11 +506,6 @@
    8.21  
    8.22  (** Isar command syntax **)
    8.23  
    8.24 -fun proof_state st =
    8.25 -  (case try Toplevel.proof_of st of
    8.26 -    SOME state => state
    8.27 -  | NONE => Proof.init (Toplevel.context_of st));
    8.28 -
    8.29  local
    8.30  
    8.31  val criterion =
    8.32 @@ -518,37 +517,29 @@
    8.33    Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp ||
    8.34    Parse.term >> Pattern;
    8.35  
    8.36 -val options =
    8.37 -  Scan.optional
    8.38 -    (Parse.$$$ "(" |--
    8.39 -      Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
    8.40 -        --| Parse.$$$ ")")) (NONE, true);
    8.41 -
    8.42 -val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
    8.43 -
    8.44  val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
    8.45  
    8.46  in
    8.47  
    8.48 +val query_parser = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
    8.49 +
    8.50  fun read_query pos str =
    8.51    Token.explode query_keywords pos str
    8.52    |> filter Token.is_proper
    8.53 -  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
    8.54 +  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query_parser --| Scan.ahead Parse.eof)))
    8.55    |> #1;
    8.56  
    8.57 -val _ =
    8.58 -  Outer_Syntax.command @{command_keyword find_theorems}
    8.59 -    "find theorems meeting specified criteria"
    8.60 -    (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
    8.61 -      Toplevel.keep (fn st =>
    8.62 -        Pretty.writeln (pretty_theorems (proof_state st) opt_lim rem_dups spec))));
    8.63 -
    8.64  end;
    8.65  
    8.66  
    8.67  
    8.68  (** PIDE query operation **)
    8.69  
    8.70 +fun proof_state st =
    8.71 +  (case try Toplevel.proof_of st of
    8.72 +    SOME state => state
    8.73 +  | NONE => Proof.init (Toplevel.context_of st));
    8.74 +
    8.75  val _ =
    8.76    Query_Operation.register {name = "find_theorems", pri = Task_Queue.urgent_pri}
    8.77      (fn {state = st, args, writeln_result, ...} =>
    8.78 @@ -563,4 +554,3 @@
    8.79        else error "Unknown context");
    8.80  
    8.81  end;
    8.82 -
     9.1 --- a/src/Pure/Tools/named_theorems.ML	Mon Apr 04 16:14:22 2016 +0200
     9.2 +++ b/src/Pure/Tools/named_theorems.ML	Mon Apr 04 17:02:34 2016 +0200
     9.3 @@ -93,12 +93,6 @@
     9.4        |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
     9.5    in (name, lthy') end;
     9.6  
     9.7 -val _ =
     9.8 -  Outer_Syntax.local_theory @{command_keyword named_theorems}
     9.9 -    "declare named collection of theorems"
    9.10 -    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
    9.11 -      fold (fn (b, descr) => snd o declare b descr));
    9.12 -
    9.13  
    9.14  (* ML antiquotation *)
    9.15  
    10.1 --- a/src/Pure/Tools/thm_deps.ML	Mon Apr 04 16:14:22 2016 +0200
    10.2 +++ b/src/Pure/Tools/thm_deps.ML	Mon Apr 04 17:02:34 2016 +0200
    10.3 @@ -47,12 +47,6 @@
    10.4      |> Graph_Display.display_graph_old
    10.5    end;
    10.6  
    10.7 -val _ =
    10.8 -  Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
    10.9 -    (Parse.xthms1 >> (fn args =>
   10.10 -      Toplevel.keep (fn st =>
   10.11 -        thm_deps (Toplevel.theory_of st) (Attrib.eval_thms (Toplevel.context_of st) args))));
   10.12 -
   10.13  
   10.14  (* unused_thms *)
   10.15  
   10.16 @@ -107,25 +101,4 @@
   10.17        else q) new_thms ([], Inttab.empty);
   10.18    in rev thms' end;
   10.19  
   10.20 -val thy_names =
   10.21 -  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
   10.22 -
   10.23 -val _ =
   10.24 -  Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
   10.25 -    (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
   10.26 -        Toplevel.keep (fn st =>
   10.27 -          let
   10.28 -            val thy = Toplevel.theory_of st;
   10.29 -            val ctxt = Toplevel.context_of st;
   10.30 -            fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
   10.31 -            val check = Theory.check ctxt;
   10.32 -          in
   10.33 -            unused_thms
   10.34 -              (case opt_range of
   10.35 -                NONE => (Theory.parents_of thy, [thy])
   10.36 -              | SOME (xs, NONE) => (map check xs, [thy])
   10.37 -              | SOME (xs, SOME ys) => (map check xs, map check ys))
   10.38 -            |> map pretty_thm |> Pretty.writeln_chunks
   10.39 -          end)));
   10.40 -
   10.41  end;
    11.1 --- a/src/Pure/Tools/thy_deps.ML	Mon Apr 04 16:14:22 2016 +0200
    11.2 +++ b/src/Pure/Tools/thy_deps.ML	Mon Apr 04 17:02:34 2016 +0200
    11.3 @@ -42,13 +42,4 @@
    11.4  
    11.5  val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps Theory.check;
    11.6  
    11.7 -val theory_bounds =
    11.8 -  Parse.position Parse.theory_xname >> single ||
    11.9 -  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
   11.10 -
   11.11 -val _ =
   11.12 -  Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
   11.13 -    (Scan.option theory_bounds -- Scan.option theory_bounds >>
   11.14 -      (fn args => Toplevel.keep (fn st => thy_deps_cmd (Toplevel.context_of st) args)));
   11.15 -
   11.16  end;