# HG changeset patch # User wenzelm # Date 1236716332 -3600 # Node ID c944e299eaf90d39baed555f78f9dff89dfe927c # Parent b5044aca0729154b3f443daab3dc95cc5554b065 invoke_case: proper qualification of name binding, avoiding old no_base_names; diff -r b5044aca0729 -r c944e299eaf9 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Mar 10 21:18:01 2009 +0100 +++ b/src/Pure/Isar/proof.ML Tue Mar 10 21:18:52 2009 +0100 @@ -677,18 +677,19 @@ local +fun qualified_binding a = + Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a)); + fun gen_invoke_case prep_att (name, xs, raw_atts) state = let val atts = map (prep_att (theory_of state)) raw_atts; val (asms, state') = state |> map_context_result (fn ctxt => ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs)); - val assumptions = asms |> map (fn (a, ts) => ((Binding.name a, atts), map (rpair []) ts)); + val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts)); in state' - |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names) |> assume_i assumptions |> add_binds_i AutoBind.no_facts - |> map_context (ProofContext.restore_naming (context_of state)) |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])]) end;