src/Pure/Isar/class.ML
changeset 36745 403585a89772
parent 36674 d95f39448121
child 36746 6e7704471eaa
     1.1 --- a/src/Pure/Isar/class.ML	Sat May 08 16:53:53 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sat May 08 19:14:13 2010 +0200
     1.3 @@ -202,7 +202,7 @@
     1.4        |> Expression.cert_declaration supexpr I inferred_elems;
     1.5      fun check_vars e vs = if null vs
     1.6        then error ("No type variable in part of specification element "
     1.7 -        ^ (Pretty.output o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
     1.8 +        ^ (Pretty.output NONE o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
     1.9        else ();
    1.10      fun check_element (e as Element.Fixes fxs) =
    1.11            map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs