src/Pure/Isar/expression.ML
changeset 52148 893b15200ec1
parent 52140 88a69da5d3fa
parent 52143 36ffe23b25f8
child 52153 f5773a46cf05
     1.1 --- a/src/Pure/Isar/expression.ML	Sat May 25 15:44:29 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat May 25 18:30:38 2013 +0200
     1.3 @@ -622,7 +622,7 @@
     1.4  fun aprop_tr' n c =
     1.5    let
     1.6      val c' = Lexicon.mark_const c;
     1.7 -    fun tr' T args =
     1.8 +    fun tr' (_: Proof.context) T args =
     1.9        if T <> dummyT andalso length args = n
    1.10        then Syntax.const "_aprop" $ Term.list_comb (Syntax.const c', args)
    1.11        else raise Match;
    1.12 @@ -656,7 +656,7 @@
    1.13  
    1.14      val ([pred_def], defs_thy) =
    1.15        thy
    1.16 -      |> bodyT = propT ? Sign.add_trfunsT [aprop_tr' (length args) name]
    1.17 +      |> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name]
    1.18        |> Sign.declare_const_global ((Binding.conceal binding, predT), NoSyn) |> snd
    1.19        |> Global_Theory.add_defs false
    1.20          [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];