src/Pure/Proof/proof_syntax.ML

       (Term.no_dummy_patterns t);
 
     fun prf_of [] (Bound i) = PBound i
       | prf_of Ts (Const (s, Type ("proof", _))) =
           change_type (if ty then SOME Ts else NONE)
-            (case NameSpace.explode s of
+            (case Long_Name.explode s of
                "axm" :: xs =>
                  let
-                   val name = NameSpace.implode xs;
+                   val name = Long_Name.implode xs;
                    val prop = (case AList.lookup (op =) axms name of
                        SOME prop => prop
                      | NONE => error ("Unknown axiom " ^ quote name))
                  in PAxm (name, prop, NONE) end
              | "thm" :: xs =>
-                 let val name = NameSpace.implode xs;
+                 let val name = Long_Name.implode xs;
                  in (case AList.lookup (op =) thms name of
                      SOME thm => fst (strip_combt (Thm.proof_of thm))
                    | NONE => error ("Unknown theorem " ^ quote name))
                  end
              | _ => error ("Illegal proof constant name: " ^ quote s))

 
 val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
   [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
 
 fun term_of _ (PThm (_, ((name, _, NONE), _))) =
-      Const (NameSpace.append "thm" name, proofT)
+      Const (Long_Name.append "thm" name, proofT)
   | term_of _ (PThm (_, ((name, _, SOME Ts), _))) =
-      mk_tyapp Ts (Const (NameSpace.append "thm" name, proofT))
-  | term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT)
+      mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT))
+  | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT)
   | term_of _ (PAxm (name, _, SOME Ts)) =
-      mk_tyapp Ts (Const (NameSpace.append "axm" name, proofT))
+      mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT))
   | term_of _ (PBound i) = Bound i
   | term_of Ts (Abst (s, opT, prf)) =
       let val T = the_default dummyT opT
       in Const ("Abst", (T --> proofT) --> proofT) $
         Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))

     val thm_names = map fst (PureThy.all_thms_of thy);
     val axm_names = map fst (Theory.all_axioms_of thy);
     val thy' = thy
       |> add_proof_syntax
       |> add_proof_atom_consts
-        (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names);
+        (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names);
   in
     (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
   end;
 
 fun read_term thy =

     val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy));
     val axm_names = map fst (Theory.all_axioms_of thy);
     val ctxt = thy
       |> add_proof_syntax
       |> add_proof_atom_consts
-        (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names)
+        (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
       |> ProofContext.init
       |> ProofContext.allow_dummies
       |> ProofContext.set_mode ProofContext.mode_schematic;
   in
     fn ty => fn s =>

     val axm_names = Symtab.keys (fold_proof_atoms true
       (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty);
   in
     add_proof_syntax #>
     add_proof_atom_consts
-      (map (NameSpace.append "thm") thm_names @ map (NameSpace.append "axm") axm_names)
+      (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
   end;
 
 fun proof_of full thm =
   let
     val thy = Thm.theory_of_thm thm;