| changeset 30435 | e62d6ecab6ad |
| parent 30364 | 577edc39b501 |
| child 31903 | c5221dbc40f6 |
--- a/src/Pure/Proof/proof_syntax.ML Wed Mar 11 15:38:25 2009 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Wed Mar 11 15:42:19 2009 +0100 @@ -36,8 +36,8 @@ fun add_proof_atom_consts names thy = thy - |> Sign.absolute_path - |> Sign.add_consts_i (map (fn name => (Binding.name name, proofT, NoSyn)) names); + |> Sign.root_path + |> Sign.add_consts_i (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); (** constants for application and abstraction **)