# HG changeset patch
# User wenzelm
# Date 1408038900 -7200
# Node ID 52c68f8126a8124f0f2032f862eff1633bd26006
# Parent  f620851148a96a489c1c3cbf09c8190ff39af0e7# Parent  e5bec882fdd0cd45ff85085c0e853266a28a3714
merged

diff -r f620851148a9 -r 52c68f8126a8 NEWS
--- a/NEWS	Thu Aug 14 13:21:19 2014 +0200
+++ b/NEWS	Thu Aug 14 19:55:00 2014 +0200
@@ -4,6 +4,12 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* Commands 'method_setup' and 'attribute_setup' now work within a
+local theory context.
+
+
 *** HOL ***
 
 * Sledgehammer:
diff -r f620851148a9 -r 52c68f8126a8 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Thu Aug 14 19:55:00 2014 +0200
@@ -915,7 +915,7 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def "method_setup"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "method_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
 
   @{rail \<open>
@@ -925,7 +925,7 @@
   \begin{description}
 
   \item @{command "method_setup"}~@{text "name = text description"}
-  defines a proof method in the current theory.  The given @{text
+  defines a proof method in the current context.  The given @{text
   "text"} has to be an ML expression of type
   @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
   basic parsers defined in structure @{ML_structure Args} and @{ML_structure
diff -r f620851148a9 -r 52c68f8126a8 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Thu Aug 14 19:55:00 2014 +0200
@@ -1031,7 +1031,7 @@
     @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
     @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
-    @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "attribute_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
   \begin{tabular}{rcll}
     @{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\
@@ -1093,7 +1093,7 @@
   concrete outer syntax, for example.
 
   \item @{command "attribute_setup"}~@{text "name = text description"}
-  defines an attribute in the current theory.  The given @{text
+  defines an attribute in the current context.  The given @{text
   "text"} has to be an ML expression of type
   @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
   structure @{ML_structure Args} and @{ML_structure Attrib}.
diff -r f620851148a9 -r 52c68f8126a8 src/Doc/Main/document/root.tex
--- a/src/Doc/Main/document/root.tex	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Doc/Main/document/root.tex	Thu Aug 14 19:55:00 2014 +0200
@@ -1,4 +1,5 @@
 \documentclass[12pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 
 \oddsidemargin=4.6mm
 \evensidemargin=4.6mm
@@ -15,17 +16,15 @@
 % this should be the last package used
 \usepackage{pdfsetup}
 
-% urls in roman style, theory text in math-similar italics
+% urls in roman style, theory text in math-similar italics, with literal underscore
 \urlstyle{rm}
-\isabellestyle{it}
+\isabellestyle{literal}
 
 % for uniform font size
 \renewcommand{\isastyle}{\isastyleminor}
 
 \parindent 0pt\parskip 0.5ex
 
-\renewcommand{\isacharunderscore}{\_}
-
 \usepackage{supertabular}
 
 \begin{document}
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/args.ML	Thu Aug 14 19:55:00 2014 +0200
@@ -51,7 +51,7 @@
   val named_text: (string -> string) -> string parser
   val named_typ: (string -> typ) -> typ parser
   val named_term: (string -> term) -> term parser
-  val named_fact: (string -> thm list) -> thm list parser
+  val named_fact: (string -> string option * thm list) -> thm list parser
   val named_attribute:
     (string * Position.T -> morphism -> attribute) -> (morphism -> attribute) parser
   val typ_abbrev: typ context_parser
@@ -106,7 +106,7 @@
       | SOME (Token.Text s) => Pretty.str (quote s)
       | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
       | SOME (Token.Term t) => Syntax.pretty_term ctxt t
-      | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
+      | SOME (Token.Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
       | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
   in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
 
@@ -130,7 +130,7 @@
 fun transform_values phi = map_args (Token.map_value
   (fn Token.Typ T => Token.Typ (Morphism.typ phi T)
     | Token.Term t => Token.Term (Morphism.term phi t)
-    | Token.Fact ths => Token.Fact (Morphism.fact phi ths)
+    | Token.Fact (a, ths) => Token.Fact (a, Morphism.fact phi ths)
     | Token.Attribute att => Token.Attribute (Morphism.transform phi att)
     | tok => tok));
 
@@ -212,15 +212,17 @@
 val internal_text = value (fn Token.Text s => s);
 val internal_typ = value (fn Token.Typ T => T);
 val internal_term = value (fn Token.Term t => t);
-val internal_fact = value (fn Token.Fact ths => ths);
+val internal_fact = value (fn Token.Fact (_, ths) => ths);
 val internal_attribute = value (fn Token.Attribute att => att);
 
 fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
 fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of);
 fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
 
-fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
-  alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of);
+fun named_fact get =
+  internal_fact ||
+  named >> evaluate Token.Fact (get o Token.content_of) >> #2 ||
+  alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of) >> #2;
 
 fun named_attribute att =
   internal_attribute ||
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 19:55:00 2014 +0200
@@ -38,10 +38,12 @@
   val generic_notes: string -> (binding * (thm list * src list) list) list ->
     Context.generic -> (string * thm list) list * Context.generic
   val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
+  val attribute_syntax: attribute context_parser -> Args.src -> attribute
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val local_setup: Binding.binding -> attribute context_parser -> string ->
     local_theory -> local_theory
-  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
+  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
+    local_theory -> local_theory
   val internal: (morphism -> attribute) -> src
   val add_del: attribute -> attribute -> attribute context_parser
   val thm_sel: Facts.interval list parser
@@ -101,10 +103,10 @@
 
 val get_attributes = Attributes.get o Context.Proof;
 
-fun transfer_attributes thy ctxt =
+fun transfer_attributes ctxt =
   let
-    val attribs' =
-      Name_Space.merge_tables (Attributes.get (Context.Theory thy), get_attributes ctxt);
+    val attribs0 = Attributes.get (Context.Theory (Proof_Context.theory_of ctxt));
+    val attribs' = Name_Space.merge_tables (attribs0, get_attributes ctxt);
   in Context.proof_map (Attributes.put attribs') ctxt end;
 
 fun print_attributes ctxt =
@@ -131,24 +133,12 @@
       Name_Space.define context true (binding, (att, comment)) (Attributes.get context);
   in (name, Context.the_theory (Attributes.put attribs' context)) end;
 
-fun define binding att comment lthy =
-  let
-    val standard_morphism =
-      Local_Theory.standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
-    val att0 = att o Args.transform_values standard_morphism;
-  in
-    lthy
-    |> Local_Theory.background_theory_result (define_global binding att0 comment)
-    |-> (fn name =>
-      Local_Theory.map_contexts
-        (fn _ => fn ctxt => transfer_attributes (Proof_Context.theory_of ctxt) ctxt)
-      #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
-          let
-            val naming = Name_Space.naming_of context;
-            val binding' = Morphism.binding phi binding;
-          in Attributes.map (Name_Space.alias_table naming binding' name) context end)
-      #> pair name)
-  end;
+fun define binding att comment =
+  Local_Theory.background_theory_result (define_global binding att comment)
+  #-> (fn name =>
+    Local_Theory.map_contexts (K transfer_attributes)
+    #> Local_Theory.generic_alias Attributes.map binding name
+    #> pair name);
 
 
 (* check *)
@@ -215,12 +205,13 @@
 fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
 
 fun attribute_setup name source cmt =
-  Context.theory_map (ML_Context.expression (#pos source)
+  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
+    ML_Lex.read_source false source @
+    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
+  |> ML_Context.expression (#pos source)
     "val (name, scan, comment): binding * attribute context_parser * string"
-    "Context.map_theory (Attrib.setup name scan comment)"
-    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
-      ML_Lex.read_source false source @
-      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
+    "Context.map_proof (Attrib.local_setup name scan comment)"
+  |> Context.proof_map;
 
 
 (* internal attribute *)
@@ -254,7 +245,9 @@
   let
     val get = Proof_Context.get_fact_generic context;
     val get_fact = get o Facts.Fact;
-    fun get_named pos name = get (Facts.Named ((name, pos), NONE));
+    fun get_named is_sel pos name =
+      let val (a, ths) = get (Facts.Named ((name, pos), NONE))
+      in (if is_sel then NONE else a, ths) end;
   in
     Parse.$$$ "[" |-- Args.attribs (check_name_generic context) --| Parse.$$$ "]" >> (fn srcs =>
       let
@@ -264,9 +257,9 @@
     ||
     (Scan.ahead Args.alt_name -- Args.named_fact get_fact
       >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
-     Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) =>
-      Args.named_fact (get_named pos) -- Scan.option thm_sel
-        >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
+     Scan.ahead (Parse.position fact_name -- Scan.option thm_sel) :|-- (fn ((name, pos), sel) =>
+      Args.named_fact (get_named (is_some sel) pos) --| Scan.option thm_sel
+        >> (fn fact => (name, Facts.Named ((name, pos), sel), fact))))
     -- Args.opt_attribs (check_name_generic context) >> (fn ((name, thmref, fact), srcs) =>
       let
         val ths = Facts.select thmref fact;
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 14 19:55:00 2014 +0200
@@ -39,9 +39,6 @@
   val thy_deps: Toplevel.transition -> Toplevel.transition
   val locale_deps: Toplevel.transition -> Toplevel.transition
   val class_deps: Toplevel.transition -> Toplevel.transition
-  val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
-  val unused_thms: (string list * string list option) option ->
-    Toplevel.transition -> Toplevel.transition
   val print_stmts: string list * (Facts.ref * Attrib.src list) list
     -> Toplevel.transition -> Toplevel.transition
   val print_thms: string list * (Facts.ref * Attrib.src list) list
@@ -314,28 +311,6 @@
       |> sort (int_ord o pairself #1) |> map #2;
   in Graph_Display.display_graph gr end);
 
-fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  Thm_Deps.thm_deps (Toplevel.theory_of state)
-    (Attrib.eval_thms (Toplevel.context_of state) args));
-
-
-(* find unused theorems *)
-
-fun unused_thms opt_range = Toplevel.keep (fn state =>
-  let
-    val thy = Toplevel.theory_of state;
-    val ctxt = Toplevel.context_of state;
-    fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
-    val get_theory = Context.get_theory thy;
-  in
-    Thm_Deps.unused_thms
-      (case opt_range of
-        NONE => (Theory.parents_of thy, [thy])
-      | SOME (xs, NONE) => (map get_theory xs, [thy])
-      | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
-    |> map pretty_thm |> Pretty.writeln_chunks
-  end);
-
 
 (* print theorems, terms, types etc. *)
 
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Aug 14 19:55:00 2014 +0200
@@ -329,16 +329,16 @@
     (Parse.ML_source >> Isar_Cmd.local_setup);
 
 val _ =
-  Outer_Syntax.command @{command_spec "attribute_setup"} "define attribute in ML"
+  Outer_Syntax.local_theory @{command_spec "attribute_setup"} "define attribute in ML"
     (Parse.position Parse.name --
         Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
-      >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
+      >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
 
 val _ =
-  Outer_Syntax.command @{command_spec "method_setup"} "define proof method in ML"
+  Outer_Syntax.local_theory @{command_spec "method_setup"} "define proof method in ML"
     (Parse.position Parse.name --
         Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
-      >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
+      >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "declaration"} "generic ML declaration"
@@ -894,10 +894,6 @@
     (Scan.succeed Isar_Cmd.class_deps);
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
-    (Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
-
-val _ =
   Outer_Syntax.improper_command @{command_spec "print_binds"}
     "print term bindings of proof context -- Proof General legacy"
     (Scan.succeed (Toplevel.unknown_context o
@@ -956,11 +952,6 @@
     (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
 
-val _ =
-  Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
-    (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
-       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> Isar_Cmd.unused_thms);
-
 
 
 (** system commands (for interactive mode only) **)
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Aug 14 19:55:00 2014 +0200
@@ -63,6 +63,9 @@
   val set_defsort: sort -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
+  val generic_alias:
+    (('a Name_Space.table -> 'a Name_Space.table) -> Context.generic -> Context.generic) ->
+    binding -> string -> local_theory -> local_theory
   val class_alias: binding -> class -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
@@ -102,7 +105,8 @@
   target: Proof.context};
 
 fun make_lthy (naming, operations, after_close, brittle, target) : lthy =
-  {naming = naming, operations = operations, after_close = after_close, brittle = brittle, target = target};
+  {naming = naming, operations = operations, after_close = after_close,
+    brittle = brittle, target = target};
 
 
 (* context data *)
@@ -167,7 +171,7 @@
 
 fun mark_brittle lthy =
   if level lthy = 1 then
-    map_top (fn (naming, operations, after_close, brittle, target) =>
+    map_top (fn (naming, operations, after_close, _, target) =>
       (naming, operations, after_close, true, target)) lthy
   else lthy;
 
@@ -254,12 +258,12 @@
 
 val operations_of = #operations o top_of;
 
+fun operation f lthy = f (operations_of lthy) lthy;
+fun operation2 f x y = operation (fn ops => f ops x y);
+
 
 (* primitives *)
 
-fun operation f lthy = f (operations_of lthy) lthy;
-fun operation2 f x y = operation (fn ops => f ops x y);
-
 val pretty = operation #pretty;
 val abbrev = operation2 #abbrev;
 val define = operation2 #define false;
@@ -270,7 +274,7 @@
   assert_bottom true #> operation (fn ops => #subscription ops dep_morph mixin export);
 
 
-(* basic derived operations *)
+(* theorems *)
 
 val notes = notes_kind "";
 fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
@@ -289,6 +293,9 @@
           (Proof_Context.fact_alias binding' name)
       end));
 
+
+(* default sort *)
+
 fun set_defsort S =
   declaration {syntax = true, pervasive = false}
     (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
@@ -315,14 +322,21 @@
 
 (* name space aliases *)
 
-fun alias global_alias local_alias b name =
+fun generic_alias app b name =
+  declaration {syntax = false, pervasive = false} (fn phi => fn context =>
+    let
+      val naming = Name_Space.naming_of context;
+      val b' = Morphism.binding phi b;
+    in app (Name_Space.alias_table naming b' name) context end);
+
+fun syntax_alias global_alias local_alias b name =
   declaration {syntax = true, pervasive = false} (fn phi =>
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);
 
-val class_alias = alias Sign.class_alias Proof_Context.class_alias;
-val type_alias = alias Sign.type_alias Proof_Context.type_alias;
-val const_alias = alias Sign.const_alias Proof_Context.const_alias;
+val class_alias = syntax_alias Sign.class_alias Proof_Context.class_alias;
+val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
+val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
 
 
 
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/method.ML	Thu Aug 14 19:55:00 2014 +0200
@@ -66,8 +66,12 @@
   val check_name: Proof.context -> xstring * Position.T -> string
   val method: Proof.context -> src -> Proof.context -> method
   val method_cmd: Proof.context -> src -> Proof.context -> method
+  val method_syntax: (Proof.context -> method) context_parser -> Args.src -> Proof.context -> method
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
-  val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
+  val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
+    local_theory -> local_theory
+  val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
+    local_theory -> local_theory
   type modifier = (Proof.context -> Proof.context) * attribute
   val section: modifier parser list -> thm list context_parser
   val sections: modifier parser list -> thm list list context_parser
@@ -309,7 +313,7 @@
 
 (* method definitions *)
 
-structure Methods = Theory_Data
+structure Methods = Generic_Data
 (
   type T = ((src -> Proof.context -> method) * string) Name_Space.table;
   val empty : T = Name_Space.empty_table "method";
@@ -317,7 +321,13 @@
   fun merge data : T = Name_Space.merge_tables data;
 );
 
-val get_methods = Methods.get o Proof_Context.theory_of;
+val get_methods = Methods.get o Context.Proof;
+
+fun transfer_methods ctxt =
+  let
+    val meths0 = Methods.get (Context.Theory (Proof_Context.theory_of ctxt));
+    val meths' = Name_Space.merge_tables (meths0, get_methods ctxt);
+  in Context.proof_map (Methods.put meths') ctxt end;
 
 fun print_methods ctxt =
   let
@@ -331,8 +341,22 @@
     |> Pretty.writeln_chunks
   end;
 
-fun add_method name meth comment thy = thy
-  |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
+
+(* define *)
+
+fun define_global binding meth comment thy =
+  let
+    val context = Context.Theory thy;
+    val (name, meths') =
+      Name_Space.define context true (binding, (meth, comment)) (Methods.get context);
+  in (name, Context.the_theory (Methods.put meths' context)) end;
+
+fun define binding meth comment =
+  Local_Theory.background_theory_result (define_global binding meth comment)
+  #-> (fn name =>
+    Local_Theory.map_contexts (K transfer_methods)
+    #> Local_Theory.generic_alias Methods.map binding name
+    #> pair name);
 
 
 (* check *)
@@ -360,17 +384,20 @@
 
 (* method setup *)
 
-fun setup name scan =
-  add_method name
-    (fn src => fn ctxt => let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end);
+fun method_syntax scan src ctxt : method =
+  let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end;
+
+fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
+fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
 
 fun method_setup name source cmt =
-  Context.theory_map (ML_Context.expression (#pos source)
+  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
+    ML_Lex.read_source false source @
+    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
+  |> ML_Context.expression (#pos source)
     "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
-    "Context.map_theory (Method.setup name scan comment)"
-    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
-      ML_Lex.read_source false source @
-      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
+    "Context.map_proof (Method.local_setup name scan comment)"
+  |> Context.proof_map;
 
 
 
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Aug 14 19:55:00 2014 +0200
@@ -121,7 +121,7 @@
     (term list list * (Proof.context -> Proof.context)) * Proof.context
   val fact_tac: Proof.context -> thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
-  val get_fact_generic: Context.generic -> Facts.ref -> thm list
+  val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
   val get_fact: Proof.context -> Facts.ref -> thm list
   val get_fact_single: Proof.context -> Facts.ref -> thm
   val get_thms: Proof.context -> xstring -> thm list
@@ -948,22 +948,27 @@
             [thm] => thm
           | [] => err "Failed to retrieve literal fact"
           | _ => err "Ambiguous specification of literal fact");
-      in pick ("", Position.none) [thm] end
-  | retrieve pick context (Facts.Named ((xname, pos), ivs)) =
+      in pick true ("", Position.none) [thm] end
+  | retrieve pick context (Facts.Named ((xname, pos), sel)) =
       let
         val thy = Context.theory_of context;
-        val (name, thms) =
+        fun immediate thm = {name = xname, static = true, thms = [Thm.transfer thy thm]};
+        val {name, static, thms} =
           (case xname of
-            "" => (xname, [Thm.transfer thy Drule.dummy_thm])
-          | "_" => (xname, [Thm.transfer thy Drule.asm_rl])
+            "" => immediate Drule.dummy_thm
+          | "_" => immediate Drule.asm_rl
           | _ => retrieve_generic context (xname, pos));
-      in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end;
+        val thms' = Facts.select (Facts.Named ((name, pos), sel)) thms;
+      in pick (static orelse is_some sel) (name, pos) thms' end;
 
 in
 
-val get_fact_generic = retrieve (K I);
-val get_fact = retrieve (K I) o Context.Proof;
-val get_fact_single = retrieve Facts.the_single o Context.Proof;
+val get_fact_generic =
+  retrieve (fn static => fn (name, _) => fn thms =>
+    (if static then NONE else SOME name, thms));
+
+val get_fact = retrieve (K (K I)) o Context.Proof;
+val get_fact_single = retrieve (K Facts.the_single) o Context.Proof;
 
 fun get_thms ctxt = get_fact ctxt o Facts.named;
 fun get_thm ctxt = get_fact_single ctxt o Facts.named;
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/token.ML	Thu Aug 14 19:55:00 2014 +0200
@@ -12,7 +12,8 @@
     Error of string | Sync | EOF
   type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
   datatype value =
-    Literal of bool * Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list |
+    Literal of bool * Markup.T | Text of string | Typ of typ | Term of term |
+    Fact of string option * thm list |
     Attribute of morphism -> attribute | Files of file Exn.result list
   type T
   val str_of_kind: kind -> string
@@ -57,7 +58,7 @@
   val mk_text: string -> T
   val mk_typ: typ -> T
   val mk_term: term -> T
-  val mk_fact: thm list -> T
+  val mk_fact: string option * thm list -> T
   val mk_attribute: (morphism -> attribute) -> T
   val init_assignable: T -> T
   val assign: value option -> T -> unit
@@ -91,7 +92,7 @@
   Text of string |
   Typ of typ |
   Term of term |
-  Fact of thm list |
+  Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
   Attribute of morphism -> attribute |
   Files of file Exn.result list;
 
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Pure.thy	Thu Aug 14 19:55:00 2014 +0200
@@ -112,6 +112,7 @@
 ML_file "Isar/calculation.ML"
 ML_file "Tools/rail.ML"
 ML_file "Tools/rule_insts.ML";
+ML_file "Tools/thm_deps.ML";
 ML_file "Tools/find_theorems.ML"
 ML_file "Tools/find_consts.ML"
 ML_file "Tools/proof_general_pure.ML"
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/ROOT	Thu Aug 14 19:55:00 2014 +0200
@@ -202,7 +202,6 @@
     "Thy/latex.ML"
     "Thy/present.ML"
     "Thy/term_style.ML"
-    "Thy/thm_deps.ML"
     "Thy/thy_header.ML"
     "Thy/thy_info.ML"
     "Thy/thy_output.ML"
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/ROOT.ML	Thu Aug 14 19:55:00 2014 +0200
@@ -310,7 +310,6 @@
 use "PIDE/document.ML";
 
 (*theory and proof operations*)
-use "Thy/thm_deps.ML";
 use "Isar/isar_cmd.ML";
 
 use "subgoal.ML";
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Thu Aug 14 13:21:19 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-(*  Title:      Pure/Thy/thm_deps.ML
-    Author:     Stefan Berghofer, TU Muenchen
-
-Visualize dependencies of theorems.
-*)
-
-signature THM_DEPS =
-sig
-  val thm_deps: theory -> thm list -> unit
-  val unused_thms: theory list * theory list -> (string * thm) list
-end;
-
-structure Thm_Deps: THM_DEPS =
-struct
-
-(* thm_deps *)
-
-fun thm_deps thy thms =
-  let
-    fun add_dep ("", _, _) = I
-      | add_dep (name, _, PBody {thms = thms', ...}) =
-          let
-            val prefix = #1 (split_last (Long_Name.explode name));
-            val session =
-              (case prefix of
-                a :: _ =>
-                  (case try (Context.get_theory thy) a of
-                    SOME thy =>
-                      (case Present.session_name thy of
-                        "" => []
-                      | session => [session])
-                  | NONE => [])
-               | _ => ["global"]);
-            val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
-            val entry =
-              {name = Long_Name.base_name name,
-               ID = name,
-               dir = space_implode "/" (session @ prefix),
-               unfold = false,
-               path = "",
-               parents = parents,
-               content = []};
-          in cons entry end;
-    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
-  in Graph_Display.display_graph (sort_wrt #ID deps) end;
-
-
-(* unused_thms *)
-
-fun unused_thms (base_thys, thys) =
-  let
-    fun add_fact space (name, ths) =
-      if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
-      else
-        let val {concealed, group, ...} = Name_Space.the_entry space name in
-          fold_rev (fn th =>
-            (case Thm.derivation_name th of
-              "" => I
-            | a => cons (a, (th, concealed, group)))) ths
-        end;
-    fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
-
-    val new_thms =
-      fold (add_facts o Global_Theory.facts_of) thys []
-      |> sort_distinct (string_ord o pairself #1);
-
-    val used =
-      Proofterm.fold_body_thms
-        (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
-        (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
-        Symtab.empty;
-
-    fun is_unused a = not (Symtab.defined used a);
-
-    (* groups containing at least one used theorem *)
-    val used_groups = fold (fn (a, (_, _, group)) =>
-      if is_unused a then I
-      else
-        (case group of
-          NONE => I
-        | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
-
-    val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
-      if not concealed andalso
-        (* FIXME replace by robust treatment of thm groups *)
-        member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso
-        is_unused a
-      then
-        (case group of
-           NONE => ((a, th) :: thms, seen_groups)
-         | SOME grp =>
-             if Inttab.defined used_groups grp orelse
-               Inttab.defined seen_groups grp then q
-             else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
-      else q) new_thms ([], Inttab.empty);
-  in rev thms' end;
-
-end;
-
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/Tools/thm_deps.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/thm_deps.ML	Thu Aug 14 19:55:00 2014 +0200
@@ -0,0 +1,124 @@
+(*  Title:      Pure/Tools/thm_deps.ML
+    Author:     Stefan Berghofer, TU Muenchen
+
+Visualize dependencies of theorems.
+*)
+
+signature THM_DEPS =
+sig
+  val thm_deps: theory -> thm list -> unit
+  val unused_thms: theory list * theory list -> (string * thm) list
+end;
+
+structure Thm_Deps: THM_DEPS =
+struct
+
+(* thm_deps *)
+
+fun thm_deps thy thms =
+  let
+    fun add_dep ("", _, _) = I
+      | add_dep (name, _, PBody {thms = thms', ...}) =
+          let
+            val prefix = #1 (split_last (Long_Name.explode name));
+            val session =
+              (case prefix of
+                a :: _ =>
+                  (case try (Context.get_theory thy) a of
+                    SOME thy =>
+                      (case Present.session_name thy of
+                        "" => []
+                      | session => [session])
+                  | NONE => [])
+               | _ => ["global"]);
+            val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
+            val entry =
+              {name = Long_Name.base_name name,
+               ID = name,
+               dir = space_implode "/" (session @ prefix),
+               unfold = false,
+               path = "",
+               parents = parents,
+               content = []};
+          in cons entry end;
+    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
+  in Graph_Display.display_graph (sort_wrt #ID deps) end;
+
+val _ =
+  Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
+    (Parse_Spec.xthms1 >> (fn args =>
+      Toplevel.unknown_theory o Toplevel.keep (fn state =>
+        thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
+
+
+(* unused_thms *)
+
+fun unused_thms (base_thys, thys) =
+  let
+    fun add_fact space (name, ths) =
+      if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
+      else
+        let val {concealed, group, ...} = Name_Space.the_entry space name in
+          fold_rev (fn th =>
+            (case Thm.derivation_name th of
+              "" => I
+            | a => cons (a, (th, concealed, group)))) ths
+        end;
+    fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
+
+    val new_thms =
+      fold (add_facts o Global_Theory.facts_of) thys []
+      |> sort_distinct (string_ord o pairself #1);
+
+    val used =
+      Proofterm.fold_body_thms
+        (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
+        (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
+        Symtab.empty;
+
+    fun is_unused a = not (Symtab.defined used a);
+
+    (*groups containing at least one used theorem*)
+    val used_groups = fold (fn (a, (_, _, group)) =>
+      if is_unused a then I
+      else
+        (case group of
+          NONE => I
+        | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
+
+    val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
+      if not concealed andalso
+        (* FIXME replace by robust treatment of thm groups *)
+        member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso
+        is_unused a
+      then
+        (case group of
+           NONE => ((a, th) :: thms, seen_groups)
+         | SOME grp =>
+             if Inttab.defined used_groups grp orelse
+               Inttab.defined seen_groups grp then q
+             else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
+      else q) new_thms ([], Inttab.empty);
+  in rev thms' end;
+
+val _ =
+  Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
+    (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
+       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
+        Toplevel.keep (fn state =>
+          let
+            val thy = Toplevel.theory_of state;
+            val ctxt = Toplevel.context_of state;
+            fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
+            val get_theory = Context.get_theory thy;
+          in
+            unused_thms
+              (case opt_range of
+                NONE => (Theory.parents_of thy, [thy])
+              | SOME (xs, NONE) => (map get_theory xs, [thy])
+              | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
+            |> map pretty_thm |> Pretty.writeln_chunks
+          end)));
+
+end;
+
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/facts.ML	Thu Aug 14 19:55:00 2014 +0200
@@ -29,7 +29,8 @@
   val extern: Proof.context -> T -> string -> xstring
   val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
   val lookup: Context.generic -> T -> string -> (bool * thm list) option
-  val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list
+  val retrieve: Context.generic -> T -> xstring * Position.T ->
+    {name: string, static: bool, thms: thm list}
   val defined: T -> string -> bool
   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   val dest_static: bool -> T list -> T -> (string * thm list) list
@@ -176,14 +177,18 @@
 fun retrieve context facts (xname, pos) =
   let
     val name = check context facts (xname, pos);
-    val thms =
+    val (static, thms) =
       (case lookup context facts name of
         SOME (static, thms) =>
           (if static then ()
            else Context_Position.report_generic context pos (Markup.dynamic_fact name);
-           thms)
+           (static, thms))
       | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
-  in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
+  in
+   {name = name,
+    static = static,
+    thms = map (Thm.transfer (Context.theory_of context)) thms}
+  end;
 
 
 (* static content *)
diff -r f620851148a9 -r 52c68f8126a8 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/global_theory.ML	Thu Aug 14 19:55:00 2014 +0200
@@ -72,7 +72,7 @@
 (* retrieve theorems *)
 
 fun get_thms thy xname =
-  #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
+  #thms (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
 
 fun get_thm thy xname =
   Facts.the_single (xname, Position.none) (get_thms thy xname);