merged
authorwenzelm
Thu Aug 14 19:55:00 2014 +0200 (2014-08-14)
changeset 5794352c68f8126a8
parent 57933 f620851148a9
parent 57942 e5bec882fdd0
child 57944 fff8d328da56
merged
src/Pure/Thy/thm_deps.ML
     1.1 --- a/NEWS	Thu Aug 14 13:21:19 2014 +0200
     1.2 +++ b/NEWS	Thu Aug 14 19:55:00 2014 +0200
     1.3 @@ -4,6 +4,12 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Commands 'method_setup' and 'attribute_setup' now work within a
    1.10 +local theory context.
    1.11 +
    1.12 +
    1.13  *** HOL ***
    1.14  
    1.15  * Sledgehammer:
     2.1 --- a/src/Doc/Isar_Ref/Proof.thy	Thu Aug 14 13:21:19 2014 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Thu Aug 14 19:55:00 2014 +0200
     2.3 @@ -915,7 +915,7 @@
     2.4  
     2.5  text {*
     2.6    \begin{matharray}{rcl}
     2.7 -    @{command_def "method_setup"} & : & @{text "theory \<rightarrow> theory"} \\
     2.8 +    @{command_def "method_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.9    \end{matharray}
    2.10  
    2.11    @{rail \<open>
    2.12 @@ -925,7 +925,7 @@
    2.13    \begin{description}
    2.14  
    2.15    \item @{command "method_setup"}~@{text "name = text description"}
    2.16 -  defines a proof method in the current theory.  The given @{text
    2.17 +  defines a proof method in the current context.  The given @{text
    2.18    "text"} has to be an ML expression of type
    2.19    @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
    2.20    basic parsers defined in structure @{ML_structure Args} and @{ML_structure
     3.1 --- a/src/Doc/Isar_Ref/Spec.thy	Thu Aug 14 13:21:19 2014 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Thu Aug 14 19:55:00 2014 +0200
     3.3 @@ -1031,7 +1031,7 @@
     3.4      @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
     3.5      @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
     3.6      @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     3.7 -    @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
     3.8 +    @{command_def "attribute_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     3.9    \end{matharray}
    3.10    \begin{tabular}{rcll}
    3.11      @{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\
    3.12 @@ -1093,7 +1093,7 @@
    3.13    concrete outer syntax, for example.
    3.14  
    3.15    \item @{command "attribute_setup"}~@{text "name = text description"}
    3.16 -  defines an attribute in the current theory.  The given @{text
    3.17 +  defines an attribute in the current context.  The given @{text
    3.18    "text"} has to be an ML expression of type
    3.19    @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
    3.20    structure @{ML_structure Args} and @{ML_structure Attrib}.
     4.1 --- a/src/Doc/Main/document/root.tex	Thu Aug 14 13:21:19 2014 +0200
     4.2 +++ b/src/Doc/Main/document/root.tex	Thu Aug 14 19:55:00 2014 +0200
     4.3 @@ -1,4 +1,5 @@
     4.4  \documentclass[12pt,a4paper]{article}
     4.5 +\usepackage[T1]{fontenc}
     4.6  
     4.7  \oddsidemargin=4.6mm
     4.8  \evensidemargin=4.6mm
     4.9 @@ -15,17 +16,15 @@
    4.10  % this should be the last package used
    4.11  \usepackage{pdfsetup}
    4.12  
    4.13 -% urls in roman style, theory text in math-similar italics
    4.14 +% urls in roman style, theory text in math-similar italics, with literal underscore
    4.15  \urlstyle{rm}
    4.16 -\isabellestyle{it}
    4.17 +\isabellestyle{literal}
    4.18  
    4.19  % for uniform font size
    4.20  \renewcommand{\isastyle}{\isastyleminor}
    4.21  
    4.22  \parindent 0pt\parskip 0.5ex
    4.23  
    4.24 -\renewcommand{\isacharunderscore}{\_}
    4.25 -
    4.26  \usepackage{supertabular}
    4.27  
    4.28  \begin{document}
     5.1 --- a/src/Pure/Isar/args.ML	Thu Aug 14 13:21:19 2014 +0200
     5.2 +++ b/src/Pure/Isar/args.ML	Thu Aug 14 19:55:00 2014 +0200
     5.3 @@ -51,7 +51,7 @@
     5.4    val named_text: (string -> string) -> string parser
     5.5    val named_typ: (string -> typ) -> typ parser
     5.6    val named_term: (string -> term) -> term parser
     5.7 -  val named_fact: (string -> thm list) -> thm list parser
     5.8 +  val named_fact: (string -> string option * thm list) -> thm list parser
     5.9    val named_attribute:
    5.10      (string * Position.T -> morphism -> attribute) -> (morphism -> attribute) parser
    5.11    val typ_abbrev: typ context_parser
    5.12 @@ -106,7 +106,7 @@
    5.13        | SOME (Token.Text s) => Pretty.str (quote s)
    5.14        | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
    5.15        | SOME (Token.Term t) => Syntax.pretty_term ctxt t
    5.16 -      | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
    5.17 +      | SOME (Token.Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
    5.18        | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
    5.19    in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
    5.20  
    5.21 @@ -130,7 +130,7 @@
    5.22  fun transform_values phi = map_args (Token.map_value
    5.23    (fn Token.Typ T => Token.Typ (Morphism.typ phi T)
    5.24      | Token.Term t => Token.Term (Morphism.term phi t)
    5.25 -    | Token.Fact ths => Token.Fact (Morphism.fact phi ths)
    5.26 +    | Token.Fact (a, ths) => Token.Fact (a, Morphism.fact phi ths)
    5.27      | Token.Attribute att => Token.Attribute (Morphism.transform phi att)
    5.28      | tok => tok));
    5.29  
    5.30 @@ -212,15 +212,17 @@
    5.31  val internal_text = value (fn Token.Text s => s);
    5.32  val internal_typ = value (fn Token.Typ T => T);
    5.33  val internal_term = value (fn Token.Term t => t);
    5.34 -val internal_fact = value (fn Token.Fact ths => ths);
    5.35 +val internal_fact = value (fn Token.Fact (_, ths) => ths);
    5.36  val internal_attribute = value (fn Token.Attribute att => att);
    5.37  
    5.38  fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
    5.39  fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of);
    5.40  fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
    5.41  
    5.42 -fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
    5.43 -  alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of);
    5.44 +fun named_fact get =
    5.45 +  internal_fact ||
    5.46 +  named >> evaluate Token.Fact (get o Token.content_of) >> #2 ||
    5.47 +  alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of) >> #2;
    5.48  
    5.49  fun named_attribute att =
    5.50    internal_attribute ||
     6.1 --- a/src/Pure/Isar/attrib.ML	Thu Aug 14 13:21:19 2014 +0200
     6.2 +++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 19:55:00 2014 +0200
     6.3 @@ -38,10 +38,12 @@
     6.4    val generic_notes: string -> (binding * (thm list * src list) list) list ->
     6.5      Context.generic -> (string * thm list) list * Context.generic
     6.6    val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
     6.7 +  val attribute_syntax: attribute context_parser -> Args.src -> attribute
     6.8    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
     6.9    val local_setup: Binding.binding -> attribute context_parser -> string ->
    6.10      local_theory -> local_theory
    6.11 -  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
    6.12 +  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
    6.13 +    local_theory -> local_theory
    6.14    val internal: (morphism -> attribute) -> src
    6.15    val add_del: attribute -> attribute -> attribute context_parser
    6.16    val thm_sel: Facts.interval list parser
    6.17 @@ -101,10 +103,10 @@
    6.18  
    6.19  val get_attributes = Attributes.get o Context.Proof;
    6.20  
    6.21 -fun transfer_attributes thy ctxt =
    6.22 +fun transfer_attributes ctxt =
    6.23    let
    6.24 -    val attribs' =
    6.25 -      Name_Space.merge_tables (Attributes.get (Context.Theory thy), get_attributes ctxt);
    6.26 +    val attribs0 = Attributes.get (Context.Theory (Proof_Context.theory_of ctxt));
    6.27 +    val attribs' = Name_Space.merge_tables (attribs0, get_attributes ctxt);
    6.28    in Context.proof_map (Attributes.put attribs') ctxt end;
    6.29  
    6.30  fun print_attributes ctxt =
    6.31 @@ -131,24 +133,12 @@
    6.32        Name_Space.define context true (binding, (att, comment)) (Attributes.get context);
    6.33    in (name, Context.the_theory (Attributes.put attribs' context)) end;
    6.34  
    6.35 -fun define binding att comment lthy =
    6.36 -  let
    6.37 -    val standard_morphism =
    6.38 -      Local_Theory.standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
    6.39 -    val att0 = att o Args.transform_values standard_morphism;
    6.40 -  in
    6.41 -    lthy
    6.42 -    |> Local_Theory.background_theory_result (define_global binding att0 comment)
    6.43 -    |-> (fn name =>
    6.44 -      Local_Theory.map_contexts
    6.45 -        (fn _ => fn ctxt => transfer_attributes (Proof_Context.theory_of ctxt) ctxt)
    6.46 -      #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
    6.47 -          let
    6.48 -            val naming = Name_Space.naming_of context;
    6.49 -            val binding' = Morphism.binding phi binding;
    6.50 -          in Attributes.map (Name_Space.alias_table naming binding' name) context end)
    6.51 -      #> pair name)
    6.52 -  end;
    6.53 +fun define binding att comment =
    6.54 +  Local_Theory.background_theory_result (define_global binding att comment)
    6.55 +  #-> (fn name =>
    6.56 +    Local_Theory.map_contexts (K transfer_attributes)
    6.57 +    #> Local_Theory.generic_alias Attributes.map binding name
    6.58 +    #> pair name);
    6.59  
    6.60  
    6.61  (* check *)
    6.62 @@ -215,12 +205,13 @@
    6.63  fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
    6.64  
    6.65  fun attribute_setup name source cmt =
    6.66 -  Context.theory_map (ML_Context.expression (#pos source)
    6.67 +  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
    6.68 +    ML_Lex.read_source false source @
    6.69 +    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
    6.70 +  |> ML_Context.expression (#pos source)
    6.71      "val (name, scan, comment): binding * attribute context_parser * string"
    6.72 -    "Context.map_theory (Attrib.setup name scan comment)"
    6.73 -    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
    6.74 -      ML_Lex.read_source false source @
    6.75 -      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
    6.76 +    "Context.map_proof (Attrib.local_setup name scan comment)"
    6.77 +  |> Context.proof_map;
    6.78  
    6.79  
    6.80  (* internal attribute *)
    6.81 @@ -254,7 +245,9 @@
    6.82    let
    6.83      val get = Proof_Context.get_fact_generic context;
    6.84      val get_fact = get o Facts.Fact;
    6.85 -    fun get_named pos name = get (Facts.Named ((name, pos), NONE));
    6.86 +    fun get_named is_sel pos name =
    6.87 +      let val (a, ths) = get (Facts.Named ((name, pos), NONE))
    6.88 +      in (if is_sel then NONE else a, ths) end;
    6.89    in
    6.90      Parse.$$$ "[" |-- Args.attribs (check_name_generic context) --| Parse.$$$ "]" >> (fn srcs =>
    6.91        let
    6.92 @@ -264,9 +257,9 @@
    6.93      ||
    6.94      (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    6.95        >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
    6.96 -     Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) =>
    6.97 -      Args.named_fact (get_named pos) -- Scan.option thm_sel
    6.98 -        >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
    6.99 +     Scan.ahead (Parse.position fact_name -- Scan.option thm_sel) :|-- (fn ((name, pos), sel) =>
   6.100 +      Args.named_fact (get_named (is_some sel) pos) --| Scan.option thm_sel
   6.101 +        >> (fn fact => (name, Facts.Named ((name, pos), sel), fact))))
   6.102      -- Args.opt_attribs (check_name_generic context) >> (fn ((name, thmref, fact), srcs) =>
   6.103        let
   6.104          val ths = Facts.select thmref fact;
     7.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Aug 14 13:21:19 2014 +0200
     7.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 14 19:55:00 2014 +0200
     7.3 @@ -39,9 +39,6 @@
     7.4    val thy_deps: Toplevel.transition -> Toplevel.transition
     7.5    val locale_deps: Toplevel.transition -> Toplevel.transition
     7.6    val class_deps: Toplevel.transition -> Toplevel.transition
     7.7 -  val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
     7.8 -  val unused_thms: (string list * string list option) option ->
     7.9 -    Toplevel.transition -> Toplevel.transition
    7.10    val print_stmts: string list * (Facts.ref * Attrib.src list) list
    7.11      -> Toplevel.transition -> Toplevel.transition
    7.12    val print_thms: string list * (Facts.ref * Attrib.src list) list
    7.13 @@ -314,28 +311,6 @@
    7.14        |> sort (int_ord o pairself #1) |> map #2;
    7.15    in Graph_Display.display_graph gr end);
    7.16  
    7.17 -fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    7.18 -  Thm_Deps.thm_deps (Toplevel.theory_of state)
    7.19 -    (Attrib.eval_thms (Toplevel.context_of state) args));
    7.20 -
    7.21 -
    7.22 -(* find unused theorems *)
    7.23 -
    7.24 -fun unused_thms opt_range = Toplevel.keep (fn state =>
    7.25 -  let
    7.26 -    val thy = Toplevel.theory_of state;
    7.27 -    val ctxt = Toplevel.context_of state;
    7.28 -    fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
    7.29 -    val get_theory = Context.get_theory thy;
    7.30 -  in
    7.31 -    Thm_Deps.unused_thms
    7.32 -      (case opt_range of
    7.33 -        NONE => (Theory.parents_of thy, [thy])
    7.34 -      | SOME (xs, NONE) => (map get_theory xs, [thy])
    7.35 -      | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
    7.36 -    |> map pretty_thm |> Pretty.writeln_chunks
    7.37 -  end);
    7.38 -
    7.39  
    7.40  (* print theorems, terms, types etc. *)
    7.41  
     8.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Aug 14 13:21:19 2014 +0200
     8.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Aug 14 19:55:00 2014 +0200
     8.3 @@ -329,16 +329,16 @@
     8.4      (Parse.ML_source >> Isar_Cmd.local_setup);
     8.5  
     8.6  val _ =
     8.7 -  Outer_Syntax.command @{command_spec "attribute_setup"} "define attribute in ML"
     8.8 +  Outer_Syntax.local_theory @{command_spec "attribute_setup"} "define attribute in ML"
     8.9      (Parse.position Parse.name --
    8.10          Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
    8.11 -      >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
    8.12 +      >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
    8.13  
    8.14  val _ =
    8.15 -  Outer_Syntax.command @{command_spec "method_setup"} "define proof method in ML"
    8.16 +  Outer_Syntax.local_theory @{command_spec "method_setup"} "define proof method in ML"
    8.17      (Parse.position Parse.name --
    8.18          Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
    8.19 -      >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
    8.20 +      >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
    8.21  
    8.22  val _ =
    8.23    Outer_Syntax.local_theory @{command_spec "declaration"} "generic ML declaration"
    8.24 @@ -894,10 +894,6 @@
    8.25      (Scan.succeed Isar_Cmd.class_deps);
    8.26  
    8.27  val _ =
    8.28 -  Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
    8.29 -    (Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
    8.30 -
    8.31 -val _ =
    8.32    Outer_Syntax.improper_command @{command_spec "print_binds"}
    8.33      "print term bindings of proof context -- Proof General legacy"
    8.34      (Scan.succeed (Toplevel.unknown_context o
    8.35 @@ -956,11 +952,6 @@
    8.36      (Scan.succeed (Toplevel.unknown_theory o
    8.37        Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
    8.38  
    8.39 -val _ =
    8.40 -  Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
    8.41 -    (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
    8.42 -       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> Isar_Cmd.unused_thms);
    8.43 -
    8.44  
    8.45  
    8.46  (** system commands (for interactive mode only) **)
     9.1 --- a/src/Pure/Isar/local_theory.ML	Thu Aug 14 13:21:19 2014 +0200
     9.2 +++ b/src/Pure/Isar/local_theory.ML	Thu Aug 14 19:55:00 2014 +0200
     9.3 @@ -63,6 +63,9 @@
     9.4    val set_defsort: sort -> local_theory -> local_theory
     9.5    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
     9.6    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     9.7 +  val generic_alias:
     9.8 +    (('a Name_Space.table -> 'a Name_Space.table) -> Context.generic -> Context.generic) ->
     9.9 +    binding -> string -> local_theory -> local_theory
    9.10    val class_alias: binding -> class -> local_theory -> local_theory
    9.11    val type_alias: binding -> string -> local_theory -> local_theory
    9.12    val const_alias: binding -> string -> local_theory -> local_theory
    9.13 @@ -102,7 +105,8 @@
    9.14    target: Proof.context};
    9.15  
    9.16  fun make_lthy (naming, operations, after_close, brittle, target) : lthy =
    9.17 -  {naming = naming, operations = operations, after_close = after_close, brittle = brittle, target = target};
    9.18 +  {naming = naming, operations = operations, after_close = after_close,
    9.19 +    brittle = brittle, target = target};
    9.20  
    9.21  
    9.22  (* context data *)
    9.23 @@ -167,7 +171,7 @@
    9.24  
    9.25  fun mark_brittle lthy =
    9.26    if level lthy = 1 then
    9.27 -    map_top (fn (naming, operations, after_close, brittle, target) =>
    9.28 +    map_top (fn (naming, operations, after_close, _, target) =>
    9.29        (naming, operations, after_close, true, target)) lthy
    9.30    else lthy;
    9.31  
    9.32 @@ -254,12 +258,12 @@
    9.33  
    9.34  val operations_of = #operations o top_of;
    9.35  
    9.36 +fun operation f lthy = f (operations_of lthy) lthy;
    9.37 +fun operation2 f x y = operation (fn ops => f ops x y);
    9.38 +
    9.39  
    9.40  (* primitives *)
    9.41  
    9.42 -fun operation f lthy = f (operations_of lthy) lthy;
    9.43 -fun operation2 f x y = operation (fn ops => f ops x y);
    9.44 -
    9.45  val pretty = operation #pretty;
    9.46  val abbrev = operation2 #abbrev;
    9.47  val define = operation2 #define false;
    9.48 @@ -270,7 +274,7 @@
    9.49    assert_bottom true #> operation (fn ops => #subscription ops dep_morph mixin export);
    9.50  
    9.51  
    9.52 -(* basic derived operations *)
    9.53 +(* theorems *)
    9.54  
    9.55  val notes = notes_kind "";
    9.56  fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
    9.57 @@ -289,6 +293,9 @@
    9.58            (Proof_Context.fact_alias binding' name)
    9.59        end));
    9.60  
    9.61 +
    9.62 +(* default sort *)
    9.63 +
    9.64  fun set_defsort S =
    9.65    declaration {syntax = true, pervasive = false}
    9.66      (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
    9.67 @@ -315,14 +322,21 @@
    9.68  
    9.69  (* name space aliases *)
    9.70  
    9.71 -fun alias global_alias local_alias b name =
    9.72 +fun generic_alias app b name =
    9.73 +  declaration {syntax = false, pervasive = false} (fn phi => fn context =>
    9.74 +    let
    9.75 +      val naming = Name_Space.naming_of context;
    9.76 +      val b' = Morphism.binding phi b;
    9.77 +    in app (Name_Space.alias_table naming b' name) context end);
    9.78 +
    9.79 +fun syntax_alias global_alias local_alias b name =
    9.80    declaration {syntax = true, pervasive = false} (fn phi =>
    9.81      let val b' = Morphism.binding phi b
    9.82      in Context.mapping (global_alias b' name) (local_alias b' name) end);
    9.83  
    9.84 -val class_alias = alias Sign.class_alias Proof_Context.class_alias;
    9.85 -val type_alias = alias Sign.type_alias Proof_Context.type_alias;
    9.86 -val const_alias = alias Sign.const_alias Proof_Context.const_alias;
    9.87 +val class_alias = syntax_alias Sign.class_alias Proof_Context.class_alias;
    9.88 +val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
    9.89 +val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
    9.90  
    9.91  
    9.92  
    10.1 --- a/src/Pure/Isar/method.ML	Thu Aug 14 13:21:19 2014 +0200
    10.2 +++ b/src/Pure/Isar/method.ML	Thu Aug 14 19:55:00 2014 +0200
    10.3 @@ -66,8 +66,12 @@
    10.4    val check_name: Proof.context -> xstring * Position.T -> string
    10.5    val method: Proof.context -> src -> Proof.context -> method
    10.6    val method_cmd: Proof.context -> src -> Proof.context -> method
    10.7 +  val method_syntax: (Proof.context -> method) context_parser -> Args.src -> Proof.context -> method
    10.8    val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
    10.9 -  val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
   10.10 +  val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
   10.11 +    local_theory -> local_theory
   10.12 +  val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
   10.13 +    local_theory -> local_theory
   10.14    type modifier = (Proof.context -> Proof.context) * attribute
   10.15    val section: modifier parser list -> thm list context_parser
   10.16    val sections: modifier parser list -> thm list list context_parser
   10.17 @@ -309,7 +313,7 @@
   10.18  
   10.19  (* method definitions *)
   10.20  
   10.21 -structure Methods = Theory_Data
   10.22 +structure Methods = Generic_Data
   10.23  (
   10.24    type T = ((src -> Proof.context -> method) * string) Name_Space.table;
   10.25    val empty : T = Name_Space.empty_table "method";
   10.26 @@ -317,7 +321,13 @@
   10.27    fun merge data : T = Name_Space.merge_tables data;
   10.28  );
   10.29  
   10.30 -val get_methods = Methods.get o Proof_Context.theory_of;
   10.31 +val get_methods = Methods.get o Context.Proof;
   10.32 +
   10.33 +fun transfer_methods ctxt =
   10.34 +  let
   10.35 +    val meths0 = Methods.get (Context.Theory (Proof_Context.theory_of ctxt));
   10.36 +    val meths' = Name_Space.merge_tables (meths0, get_methods ctxt);
   10.37 +  in Context.proof_map (Methods.put meths') ctxt end;
   10.38  
   10.39  fun print_methods ctxt =
   10.40    let
   10.41 @@ -331,8 +341,22 @@
   10.42      |> Pretty.writeln_chunks
   10.43    end;
   10.44  
   10.45 -fun add_method name meth comment thy = thy
   10.46 -  |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
   10.47 +
   10.48 +(* define *)
   10.49 +
   10.50 +fun define_global binding meth comment thy =
   10.51 +  let
   10.52 +    val context = Context.Theory thy;
   10.53 +    val (name, meths') =
   10.54 +      Name_Space.define context true (binding, (meth, comment)) (Methods.get context);
   10.55 +  in (name, Context.the_theory (Methods.put meths' context)) end;
   10.56 +
   10.57 +fun define binding meth comment =
   10.58 +  Local_Theory.background_theory_result (define_global binding meth comment)
   10.59 +  #-> (fn name =>
   10.60 +    Local_Theory.map_contexts (K transfer_methods)
   10.61 +    #> Local_Theory.generic_alias Methods.map binding name
   10.62 +    #> pair name);
   10.63  
   10.64  
   10.65  (* check *)
   10.66 @@ -360,17 +384,20 @@
   10.67  
   10.68  (* method setup *)
   10.69  
   10.70 -fun setup name scan =
   10.71 -  add_method name
   10.72 -    (fn src => fn ctxt => let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end);
   10.73 +fun method_syntax scan src ctxt : method =
   10.74 +  let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end;
   10.75 +
   10.76 +fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
   10.77 +fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
   10.78  
   10.79  fun method_setup name source cmt =
   10.80 -  Context.theory_map (ML_Context.expression (#pos source)
   10.81 +  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
   10.82 +    ML_Lex.read_source false source @
   10.83 +    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
   10.84 +  |> ML_Context.expression (#pos source)
   10.85      "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
   10.86 -    "Context.map_theory (Method.setup name scan comment)"
   10.87 -    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
   10.88 -      ML_Lex.read_source false source @
   10.89 -      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
   10.90 +    "Context.map_proof (Method.local_setup name scan comment)"
   10.91 +  |> Context.proof_map;
   10.92  
   10.93  
   10.94  
    11.1 --- a/src/Pure/Isar/proof_context.ML	Thu Aug 14 13:21:19 2014 +0200
    11.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Aug 14 19:55:00 2014 +0200
    11.3 @@ -121,7 +121,7 @@
    11.4      (term list list * (Proof.context -> Proof.context)) * Proof.context
    11.5    val fact_tac: Proof.context -> thm list -> int -> tactic
    11.6    val some_fact_tac: Proof.context -> int -> tactic
    11.7 -  val get_fact_generic: Context.generic -> Facts.ref -> thm list
    11.8 +  val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
    11.9    val get_fact: Proof.context -> Facts.ref -> thm list
   11.10    val get_fact_single: Proof.context -> Facts.ref -> thm
   11.11    val get_thms: Proof.context -> xstring -> thm list
   11.12 @@ -948,22 +948,27 @@
   11.13              [thm] => thm
   11.14            | [] => err "Failed to retrieve literal fact"
   11.15            | _ => err "Ambiguous specification of literal fact");
   11.16 -      in pick ("", Position.none) [thm] end
   11.17 -  | retrieve pick context (Facts.Named ((xname, pos), ivs)) =
   11.18 +      in pick true ("", Position.none) [thm] end
   11.19 +  | retrieve pick context (Facts.Named ((xname, pos), sel)) =
   11.20        let
   11.21          val thy = Context.theory_of context;
   11.22 -        val (name, thms) =
   11.23 +        fun immediate thm = {name = xname, static = true, thms = [Thm.transfer thy thm]};
   11.24 +        val {name, static, thms} =
   11.25            (case xname of
   11.26 -            "" => (xname, [Thm.transfer thy Drule.dummy_thm])
   11.27 -          | "_" => (xname, [Thm.transfer thy Drule.asm_rl])
   11.28 +            "" => immediate Drule.dummy_thm
   11.29 +          | "_" => immediate Drule.asm_rl
   11.30            | _ => retrieve_generic context (xname, pos));
   11.31 -      in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end;
   11.32 +        val thms' = Facts.select (Facts.Named ((name, pos), sel)) thms;
   11.33 +      in pick (static orelse is_some sel) (name, pos) thms' end;
   11.34  
   11.35  in
   11.36  
   11.37 -val get_fact_generic = retrieve (K I);
   11.38 -val get_fact = retrieve (K I) o Context.Proof;
   11.39 -val get_fact_single = retrieve Facts.the_single o Context.Proof;
   11.40 +val get_fact_generic =
   11.41 +  retrieve (fn static => fn (name, _) => fn thms =>
   11.42 +    (if static then NONE else SOME name, thms));
   11.43 +
   11.44 +val get_fact = retrieve (K (K I)) o Context.Proof;
   11.45 +val get_fact_single = retrieve (K Facts.the_single) o Context.Proof;
   11.46  
   11.47  fun get_thms ctxt = get_fact ctxt o Facts.named;
   11.48  fun get_thm ctxt = get_fact_single ctxt o Facts.named;
    12.1 --- a/src/Pure/Isar/token.ML	Thu Aug 14 13:21:19 2014 +0200
    12.2 +++ b/src/Pure/Isar/token.ML	Thu Aug 14 19:55:00 2014 +0200
    12.3 @@ -12,7 +12,8 @@
    12.4      Error of string | Sync | EOF
    12.5    type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
    12.6    datatype value =
    12.7 -    Literal of bool * Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list |
    12.8 +    Literal of bool * Markup.T | Text of string | Typ of typ | Term of term |
    12.9 +    Fact of string option * thm list |
   12.10      Attribute of morphism -> attribute | Files of file Exn.result list
   12.11    type T
   12.12    val str_of_kind: kind -> string
   12.13 @@ -57,7 +58,7 @@
   12.14    val mk_text: string -> T
   12.15    val mk_typ: typ -> T
   12.16    val mk_term: term -> T
   12.17 -  val mk_fact: thm list -> T
   12.18 +  val mk_fact: string option * thm list -> T
   12.19    val mk_attribute: (morphism -> attribute) -> T
   12.20    val init_assignable: T -> T
   12.21    val assign: value option -> T -> unit
   12.22 @@ -91,7 +92,7 @@
   12.23    Text of string |
   12.24    Typ of typ |
   12.25    Term of term |
   12.26 -  Fact of thm list |
   12.27 +  Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
   12.28    Attribute of morphism -> attribute |
   12.29    Files of file Exn.result list;
   12.30  
    13.1 --- a/src/Pure/Pure.thy	Thu Aug 14 13:21:19 2014 +0200
    13.2 +++ b/src/Pure/Pure.thy	Thu Aug 14 19:55:00 2014 +0200
    13.3 @@ -112,6 +112,7 @@
    13.4  ML_file "Isar/calculation.ML"
    13.5  ML_file "Tools/rail.ML"
    13.6  ML_file "Tools/rule_insts.ML";
    13.7 +ML_file "Tools/thm_deps.ML";
    13.8  ML_file "Tools/find_theorems.ML"
    13.9  ML_file "Tools/find_consts.ML"
   13.10  ML_file "Tools/proof_general_pure.ML"
    14.1 --- a/src/Pure/ROOT	Thu Aug 14 13:21:19 2014 +0200
    14.2 +++ b/src/Pure/ROOT	Thu Aug 14 19:55:00 2014 +0200
    14.3 @@ -202,7 +202,6 @@
    14.4      "Thy/latex.ML"
    14.5      "Thy/present.ML"
    14.6      "Thy/term_style.ML"
    14.7 -    "Thy/thm_deps.ML"
    14.8      "Thy/thy_header.ML"
    14.9      "Thy/thy_info.ML"
   14.10      "Thy/thy_output.ML"
    15.1 --- a/src/Pure/ROOT.ML	Thu Aug 14 13:21:19 2014 +0200
    15.2 +++ b/src/Pure/ROOT.ML	Thu Aug 14 19:55:00 2014 +0200
    15.3 @@ -310,7 +310,6 @@
    15.4  use "PIDE/document.ML";
    15.5  
    15.6  (*theory and proof operations*)
    15.7 -use "Thy/thm_deps.ML";
    15.8  use "Isar/isar_cmd.ML";
    15.9  
   15.10  use "subgoal.ML";
    16.1 --- a/src/Pure/Thy/thm_deps.ML	Thu Aug 14 13:21:19 2014 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,99 +0,0 @@
    16.4 -(*  Title:      Pure/Thy/thm_deps.ML
    16.5 -    Author:     Stefan Berghofer, TU Muenchen
    16.6 -
    16.7 -Visualize dependencies of theorems.
    16.8 -*)
    16.9 -
   16.10 -signature THM_DEPS =
   16.11 -sig
   16.12 -  val thm_deps: theory -> thm list -> unit
   16.13 -  val unused_thms: theory list * theory list -> (string * thm) list
   16.14 -end;
   16.15 -
   16.16 -structure Thm_Deps: THM_DEPS =
   16.17 -struct
   16.18 -
   16.19 -(* thm_deps *)
   16.20 -
   16.21 -fun thm_deps thy thms =
   16.22 -  let
   16.23 -    fun add_dep ("", _, _) = I
   16.24 -      | add_dep (name, _, PBody {thms = thms', ...}) =
   16.25 -          let
   16.26 -            val prefix = #1 (split_last (Long_Name.explode name));
   16.27 -            val session =
   16.28 -              (case prefix of
   16.29 -                a :: _ =>
   16.30 -                  (case try (Context.get_theory thy) a of
   16.31 -                    SOME thy =>
   16.32 -                      (case Present.session_name thy of
   16.33 -                        "" => []
   16.34 -                      | session => [session])
   16.35 -                  | NONE => [])
   16.36 -               | _ => ["global"]);
   16.37 -            val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
   16.38 -            val entry =
   16.39 -              {name = Long_Name.base_name name,
   16.40 -               ID = name,
   16.41 -               dir = space_implode "/" (session @ prefix),
   16.42 -               unfold = false,
   16.43 -               path = "",
   16.44 -               parents = parents,
   16.45 -               content = []};
   16.46 -          in cons entry end;
   16.47 -    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
   16.48 -  in Graph_Display.display_graph (sort_wrt #ID deps) end;
   16.49 -
   16.50 -
   16.51 -(* unused_thms *)
   16.52 -
   16.53 -fun unused_thms (base_thys, thys) =
   16.54 -  let
   16.55 -    fun add_fact space (name, ths) =
   16.56 -      if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
   16.57 -      else
   16.58 -        let val {concealed, group, ...} = Name_Space.the_entry space name in
   16.59 -          fold_rev (fn th =>
   16.60 -            (case Thm.derivation_name th of
   16.61 -              "" => I
   16.62 -            | a => cons (a, (th, concealed, group)))) ths
   16.63 -        end;
   16.64 -    fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
   16.65 -
   16.66 -    val new_thms =
   16.67 -      fold (add_facts o Global_Theory.facts_of) thys []
   16.68 -      |> sort_distinct (string_ord o pairself #1);
   16.69 -
   16.70 -    val used =
   16.71 -      Proofterm.fold_body_thms
   16.72 -        (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
   16.73 -        (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
   16.74 -        Symtab.empty;
   16.75 -
   16.76 -    fun is_unused a = not (Symtab.defined used a);
   16.77 -
   16.78 -    (* groups containing at least one used theorem *)
   16.79 -    val used_groups = fold (fn (a, (_, _, group)) =>
   16.80 -      if is_unused a then I
   16.81 -      else
   16.82 -        (case group of
   16.83 -          NONE => I
   16.84 -        | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
   16.85 -
   16.86 -    val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
   16.87 -      if not concealed andalso
   16.88 -        (* FIXME replace by robust treatment of thm groups *)
   16.89 -        member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso
   16.90 -        is_unused a
   16.91 -      then
   16.92 -        (case group of
   16.93 -           NONE => ((a, th) :: thms, seen_groups)
   16.94 -         | SOME grp =>
   16.95 -             if Inttab.defined used_groups grp orelse
   16.96 -               Inttab.defined seen_groups grp then q
   16.97 -             else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
   16.98 -      else q) new_thms ([], Inttab.empty);
   16.99 -  in rev thms' end;
  16.100 -
  16.101 -end;
  16.102 -
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/Pure/Tools/thm_deps.ML	Thu Aug 14 19:55:00 2014 +0200
    17.3 @@ -0,0 +1,124 @@
    17.4 +(*  Title:      Pure/Tools/thm_deps.ML
    17.5 +    Author:     Stefan Berghofer, TU Muenchen
    17.6 +
    17.7 +Visualize dependencies of theorems.
    17.8 +*)
    17.9 +
   17.10 +signature THM_DEPS =
   17.11 +sig
   17.12 +  val thm_deps: theory -> thm list -> unit
   17.13 +  val unused_thms: theory list * theory list -> (string * thm) list
   17.14 +end;
   17.15 +
   17.16 +structure Thm_Deps: THM_DEPS =
   17.17 +struct
   17.18 +
   17.19 +(* thm_deps *)
   17.20 +
   17.21 +fun thm_deps thy thms =
   17.22 +  let
   17.23 +    fun add_dep ("", _, _) = I
   17.24 +      | add_dep (name, _, PBody {thms = thms', ...}) =
   17.25 +          let
   17.26 +            val prefix = #1 (split_last (Long_Name.explode name));
   17.27 +            val session =
   17.28 +              (case prefix of
   17.29 +                a :: _ =>
   17.30 +                  (case try (Context.get_theory thy) a of
   17.31 +                    SOME thy =>
   17.32 +                      (case Present.session_name thy of
   17.33 +                        "" => []
   17.34 +                      | session => [session])
   17.35 +                  | NONE => [])
   17.36 +               | _ => ["global"]);
   17.37 +            val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
   17.38 +            val entry =
   17.39 +              {name = Long_Name.base_name name,
   17.40 +               ID = name,
   17.41 +               dir = space_implode "/" (session @ prefix),
   17.42 +               unfold = false,
   17.43 +               path = "",
   17.44 +               parents = parents,
   17.45 +               content = []};
   17.46 +          in cons entry end;
   17.47 +    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
   17.48 +  in Graph_Display.display_graph (sort_wrt #ID deps) end;
   17.49 +
   17.50 +val _ =
   17.51 +  Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
   17.52 +    (Parse_Spec.xthms1 >> (fn args =>
   17.53 +      Toplevel.unknown_theory o Toplevel.keep (fn state =>
   17.54 +        thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
   17.55 +
   17.56 +
   17.57 +(* unused_thms *)
   17.58 +
   17.59 +fun unused_thms (base_thys, thys) =
   17.60 +  let
   17.61 +    fun add_fact space (name, ths) =
   17.62 +      if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
   17.63 +      else
   17.64 +        let val {concealed, group, ...} = Name_Space.the_entry space name in
   17.65 +          fold_rev (fn th =>
   17.66 +            (case Thm.derivation_name th of
   17.67 +              "" => I
   17.68 +            | a => cons (a, (th, concealed, group)))) ths
   17.69 +        end;
   17.70 +    fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
   17.71 +
   17.72 +    val new_thms =
   17.73 +      fold (add_facts o Global_Theory.facts_of) thys []
   17.74 +      |> sort_distinct (string_ord o pairself #1);
   17.75 +
   17.76 +    val used =
   17.77 +      Proofterm.fold_body_thms
   17.78 +        (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
   17.79 +        (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
   17.80 +        Symtab.empty;
   17.81 +
   17.82 +    fun is_unused a = not (Symtab.defined used a);
   17.83 +
   17.84 +    (*groups containing at least one used theorem*)
   17.85 +    val used_groups = fold (fn (a, (_, _, group)) =>
   17.86 +      if is_unused a then I
   17.87 +      else
   17.88 +        (case group of
   17.89 +          NONE => I
   17.90 +        | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
   17.91 +
   17.92 +    val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
   17.93 +      if not concealed andalso
   17.94 +        (* FIXME replace by robust treatment of thm groups *)
   17.95 +        member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso
   17.96 +        is_unused a
   17.97 +      then
   17.98 +        (case group of
   17.99 +           NONE => ((a, th) :: thms, seen_groups)
  17.100 +         | SOME grp =>
  17.101 +             if Inttab.defined used_groups grp orelse
  17.102 +               Inttab.defined seen_groups grp then q
  17.103 +             else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
  17.104 +      else q) new_thms ([], Inttab.empty);
  17.105 +  in rev thms' end;
  17.106 +
  17.107 +val _ =
  17.108 +  Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
  17.109 +    (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
  17.110 +       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
  17.111 +        Toplevel.keep (fn state =>
  17.112 +          let
  17.113 +            val thy = Toplevel.theory_of state;
  17.114 +            val ctxt = Toplevel.context_of state;
  17.115 +            fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
  17.116 +            val get_theory = Context.get_theory thy;
  17.117 +          in
  17.118 +            unused_thms
  17.119 +              (case opt_range of
  17.120 +                NONE => (Theory.parents_of thy, [thy])
  17.121 +              | SOME (xs, NONE) => (map get_theory xs, [thy])
  17.122 +              | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
  17.123 +            |> map pretty_thm |> Pretty.writeln_chunks
  17.124 +          end)));
  17.125 +
  17.126 +end;
  17.127 +
    18.1 --- a/src/Pure/facts.ML	Thu Aug 14 13:21:19 2014 +0200
    18.2 +++ b/src/Pure/facts.ML	Thu Aug 14 19:55:00 2014 +0200
    18.3 @@ -29,7 +29,8 @@
    18.4    val extern: Proof.context -> T -> string -> xstring
    18.5    val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
    18.6    val lookup: Context.generic -> T -> string -> (bool * thm list) option
    18.7 -  val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list
    18.8 +  val retrieve: Context.generic -> T -> xstring * Position.T ->
    18.9 +    {name: string, static: bool, thms: thm list}
   18.10    val defined: T -> string -> bool
   18.11    val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   18.12    val dest_static: bool -> T list -> T -> (string * thm list) list
   18.13 @@ -176,14 +177,18 @@
   18.14  fun retrieve context facts (xname, pos) =
   18.15    let
   18.16      val name = check context facts (xname, pos);
   18.17 -    val thms =
   18.18 +    val (static, thms) =
   18.19        (case lookup context facts name of
   18.20          SOME (static, thms) =>
   18.21            (if static then ()
   18.22             else Context_Position.report_generic context pos (Markup.dynamic_fact name);
   18.23 -           thms)
   18.24 +           (static, thms))
   18.25        | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
   18.26 -  in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
   18.27 +  in
   18.28 +   {name = name,
   18.29 +    static = static,
   18.30 +    thms = map (Thm.transfer (Context.theory_of context)) thms}
   18.31 +  end;
   18.32  
   18.33  
   18.34  (* static content *)
    19.1 --- a/src/Pure/global_theory.ML	Thu Aug 14 13:21:19 2014 +0200
    19.2 +++ b/src/Pure/global_theory.ML	Thu Aug 14 19:55:00 2014 +0200
    19.3 @@ -72,7 +72,7 @@
    19.4  (* retrieve theorems *)
    19.5  
    19.6  fun get_thms thy xname =
    19.7 -  #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
    19.8 +  #thms (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
    19.9  
   19.10  fun get_thm thy xname =
   19.11    Facts.the_single (xname, Position.none) (get_thms thy xname);