# 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;