1.1 --- a/src/Pure/Isar/expression.ML	Thu Oct 11 16:09:44 2012 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Oct 11 19:25:36 2012 +0200
     1.3 @@ -615,11 +615,14 @@
     1.4  
     1.5  (* achieve plain syntax for locale predicates (without "PROP") *)
     1.6  
     1.7 -fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args =>
     1.8 -  if length args = n then
     1.9 -    Syntax.const "_aprop" $   (* FIXME avoid old-style early externing (!??) *)
    1.10 -      Term.list_comb (Syntax.free (Proof_Context.extern_const ctxt c), args)
    1.11 -  else raise Match);
    1.12 +fun aprop_tr' n c =
    1.13 +  let
    1.14 +    val c' = Lexicon.mark_const c;
    1.15 +    fun tr' T args =
    1.16 +      if T <> dummyT andalso length args = n
    1.17 +      then Syntax.const "_aprop" $ Term.list_comb (Syntax.const c', args)
    1.18 +      else raise Match;
    1.19 +  in (c', tr') end;
    1.20  
    1.21  (* define one predicate including its intro rule and axioms
    1.22     - binding: predicate name
    1.23 @@ -649,7 +652,7 @@
    1.24  
    1.25      val ([pred_def], defs_thy) =
    1.26        thy
    1.27 -      |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
    1.28 +      |> bodyT = propT ? Sign.add_trfunsT [aprop_tr' (length args) name]
    1.29        |> Sign.declare_const_global ((Binding.conceal binding, predT), NoSyn) |> snd
    1.30        |> Global_Theory.add_defs false
    1.31          [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];