src/Pure/Proof/proof_syntax.ML
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 **)