# HG changeset patch # User wenzelm # Date 1465326788 -7200 # Node ID 3f594efa9504d053333efe2eeca52c3b873a9700 # Parent 7bd64a07fe43ecbb09a2b04e769341ab8c174262 clarified signature; diff -r 7bd64a07fe43 -r 3f594efa9504 src/HOL/Eisbach/method_closure.ML --- a/src/HOL/Eisbach/method_closure.ML Tue Jun 07 20:45:07 2016 +0200 +++ b/src/HOL/Eisbach/method_closure.ML Tue Jun 07 21:13:08 2016 +0200 @@ -122,7 +122,7 @@ text |> (Method.map_source o map o Token.map_facts) (fn SOME name => (case Proof_Context.lookup_fact ctxt name of - SOME (false, ths) => K ths + SOME {dynamic = true, thms} => K thms | _ => I) | NONE => I); val ctxt' = Config.put Method.closure false ctxt; diff -r 7bd64a07fe43 -r 3f594efa9504 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Jun 07 20:45:07 2016 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Jun 07 21:13:08 2016 +0200 @@ -116,7 +116,7 @@ (term list list * (indexname * term) list) val fact_tac: Proof.context -> thm list -> int -> tactic val some_fact_tac: Proof.context -> int -> tactic - val lookup_fact: Proof.context -> string -> (bool * thm list) option + val lookup_fact: Proof.context -> string -> {dynamic: bool, thms: thm list} option val dynamic_facts_dummy: bool Config.T val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list val get_fact: Proof.context -> Facts.ref -> thm list @@ -1008,23 +1008,23 @@ | retrieve pick context (Facts.Named ((xname, pos), sel)) = let val thy = Context.theory_of context; - fun immediate thm = {name = xname, static = true, thms = [Thm.transfer thy thm]}; - val {name, static, thms} = + fun immediate thm = {name = xname, dynamic = false, thms = [Thm.transfer thy thm]}; + val {name, dynamic, thms} = (case xname of "" => immediate Drule.dummy_thm | "_" => immediate Drule.asm_rl | _ => retrieve_generic context (xname, pos)); val thms' = - if not static andalso Config.get_generic context dynamic_facts_dummy + if dynamic andalso Config.get_generic context dynamic_facts_dummy then [Drule.free_dummy_thm] else Facts.select (Facts.Named ((name, pos), sel)) thms; - in pick (static orelse is_some sel) (name, pos) thms' end; + in pick (dynamic andalso is_none sel) (name, pos) thms' end; in val get_fact_generic = - retrieve (fn static => fn (name, _) => fn thms => - (if static then NONE else SOME name, thms)); + retrieve (fn dynamic => fn (name, _) => fn thms => + (if dynamic then SOME name else NONE, thms)); val get_fact = retrieve (K (K I)) o Context.Proof; val get_fact_single = retrieve (K Facts.the_single) o Context.Proof; diff -r 7bd64a07fe43 -r 3f594efa9504 src/Pure/facts.ML --- a/src/Pure/facts.ML Tue Jun 07 20:45:07 2016 +0200 +++ b/src/Pure/facts.ML Tue Jun 07 21:13:08 2016 +0200 @@ -30,9 +30,9 @@ val markup_extern: Proof.context -> T -> string -> Markup.T * xstring val defined: T -> string -> bool val is_dynamic: T -> string -> bool - val lookup: Context.generic -> T -> string -> (bool * thm list) option + val lookup: Context.generic -> T -> string -> {dynamic: bool, thms: thm list} option val retrieve: Context.generic -> T -> xstring * Position.T -> - {name: string, static: bool, thms: thm list} + {name: string, dynamic: bool, thms: thm list} val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a val dest_static: bool -> T list -> T -> (string * thm list) list val dest_all: Context.generic -> bool -> T list -> T -> (string * thm list) list @@ -178,22 +178,23 @@ fun lookup context facts name = (case Name_Space.lookup (facts_of facts) name of NONE => NONE - | SOME (Static ths) => SOME (true, ths) - | SOME (Dynamic f) => SOME (false, f context)); + | SOME (Static ths) => SOME {dynamic = false, thms = ths} + | SOME (Dynamic f) => SOME {dynamic = true, thms = f context}); fun retrieve context facts (xname, pos) = let val name = check context facts (xname, pos); - val (static, thms) = + val {dynamic, thms} = (case lookup context facts name of - SOME (static, thms) => - (if static then () - else Context_Position.report_generic context pos (Markup.dynamic_fact name); - (static, thms)) + SOME res => + (if #dynamic res + then Context_Position.report_generic context pos (Markup.dynamic_fact name) + else (); + res) | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos)); in {name = name, - static = static, + dynamic = dynamic, thms = map (Thm.transfer (Context.theory_of context)) thms} end;