--- a/src/Pure/Isar/element.ML Wed Mar 11 15:45:40 2009 +0100
+++ b/src/Pure/Isar/element.ML Wed Mar 11 16:36:27 2009 +0100
@@ -518,8 +518,8 @@
fun activate elem ctxt =
let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem
in (elem', activate_elem elem' ctxt) end
- val (elems, ctxt') = fold_map activate raw_elems (ProofContext.qualified_names ctxt);
- in (elems |> map (map_ctxt_attrib Args.closure), ProofContext.restore_naming ctxt ctxt') end;
+ val (elems, ctxt') = fold_map activate raw_elems ctxt;
+ in (elems |> map (map_ctxt_attrib Args.closure), ctxt') end;
fun check_name name =
if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name)