# HG changeset patch
# User wenzelm
# Date 1192655794 -7200
# Node ID 13db30d367d299d61fa7495a4f6e6ec9d8bf60b9
# Parent  03f57b516e123833a49f44df80e9fc98b0dd0357
locale pred: authentic syntax, tuned aprop_tr' accordingly;

diff -r 03f57b516e12 -r 13db30d367d2 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Oct 17 23:16:33 2007 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Oct 17 23:16:34 2007 +0200
@@ -1677,8 +1677,10 @@
     else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
   end;
 
-fun aprop_tr' n c = (c, fn args =>
-  if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
+fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
+  if length args = n then
+    Syntax.const "_aprop" $
+      Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
   else raise Match);
 
 (* CB: define one predicate including its intro rule and axioms
@@ -1708,9 +1710,8 @@
 
     val ([pred_def], defs_thy) =
       thy
-      |> (if bodyT <> propT then I else
-        Sign.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
-      |> Sign.add_consts_i [(bname, predT, NoSyn)]
+      |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
+      |> Sign.declare_const [] (bname, predT, NoSyn) |> snd
       |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;