src/Pure/Proof/proof_syntax.ML
changeset 30364 577edc39b501
parent 30344 10a67c5ddddb
child 30435 e62d6ecab6ad
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -97,16 +97,16 @@
     1.4      fun prf_of [] (Bound i) = PBound i
     1.5        | prf_of Ts (Const (s, Type ("proof", _))) =
     1.6            change_type (if ty then SOME Ts else NONE)
     1.7 -            (case NameSpace.explode s of
     1.8 +            (case Long_Name.explode s of
     1.9                 "axm" :: xs =>
    1.10                   let
    1.11 -                   val name = NameSpace.implode xs;
    1.12 +                   val name = Long_Name.implode xs;
    1.13                     val prop = (case AList.lookup (op =) axms name of
    1.14                         SOME prop => prop
    1.15                       | NONE => error ("Unknown axiom " ^ quote name))
    1.16                   in PAxm (name, prop, NONE) end
    1.17               | "thm" :: xs =>
    1.18 -                 let val name = NameSpace.implode xs;
    1.19 +                 let val name = Long_Name.implode xs;
    1.20                   in (case AList.lookup (op =) thms name of
    1.21                       SOME thm => fst (strip_combt (Thm.proof_of thm))
    1.22                     | NONE => error ("Unknown theorem " ^ quote name))
    1.23 @@ -147,12 +147,12 @@
    1.24    [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
    1.25  
    1.26  fun term_of _ (PThm (_, ((name, _, NONE), _))) =
    1.27 -      Const (NameSpace.append "thm" name, proofT)
    1.28 +      Const (Long_Name.append "thm" name, proofT)
    1.29    | term_of _ (PThm (_, ((name, _, SOME Ts), _))) =
    1.30 -      mk_tyapp Ts (Const (NameSpace.append "thm" name, proofT))
    1.31 -  | term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT)
    1.32 +      mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT))
    1.33 +  | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT)
    1.34    | term_of _ (PAxm (name, _, SOME Ts)) =
    1.35 -      mk_tyapp Ts (Const (NameSpace.append "axm" name, proofT))
    1.36 +      mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT))
    1.37    | term_of _ (PBound i) = Bound i
    1.38    | term_of Ts (Abst (s, opT, prf)) =
    1.39        let val T = the_default dummyT opT
    1.40 @@ -183,7 +183,7 @@
    1.41      val thy' = thy
    1.42        |> add_proof_syntax
    1.43        |> add_proof_atom_consts
    1.44 -        (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names);
    1.45 +        (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names);
    1.46    in
    1.47      (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
    1.48    end;
    1.49 @@ -195,7 +195,7 @@
    1.50      val ctxt = thy
    1.51        |> add_proof_syntax
    1.52        |> add_proof_atom_consts
    1.53 -        (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names)
    1.54 +        (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
    1.55        |> ProofContext.init
    1.56        |> ProofContext.allow_dummies
    1.57        |> ProofContext.set_mode ProofContext.mode_schematic;
    1.58 @@ -219,7 +219,7 @@
    1.59    in
    1.60      add_proof_syntax #>
    1.61      add_proof_atom_consts
    1.62 -      (map (NameSpace.append "thm") thm_names @ map (NameSpace.append "axm") axm_names)
    1.63 +      (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
    1.64    end;
    1.65  
    1.66  fun proof_of full thm =