src/Pure/Isar/overloading.ML
changeset 42359 6ca5407863ed
parent 40782 aa533c5e3f48
child 42360 da8817d01e7c
     1.1 --- a/src/Pure/Isar/overloading.ML	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/Pure/Isar/overloading.ML	Sat Apr 16 15:25:25 2011 +0200
     1.3 @@ -158,11 +158,11 @@
     1.4  
     1.5  fun pretty lthy =
     1.6    let
     1.7 -    val thy = ProofContext.theory_of lthy;
     1.8      val overloading = get_overloading lthy;
     1.9      fun pr_operation ((c, ty), (v, _)) =
    1.10 -      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
    1.11 -        Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty];
    1.12 +      Pretty.block (Pretty.breaks
    1.13 +        [Pretty.str v, Pretty.str "==", Pretty.str (ProofContext.extern_const lthy c),
    1.14 +          Pretty.str "::", Syntax.pretty_typ lthy ty]);
    1.15    in Pretty.str "overloading" :: map pr_operation overloading end;
    1.16  
    1.17  fun conclude lthy =