src/Pure/ML-Systems/pp_dummy.ML
author blanchet
Fri, 23 Aug 2013 16:51:53 +0200
changeset 53159 a5805fe4e91c
parent 38635 f76ad0771f67
permissions -rw-r--r--
repaired num_extra_feature_facts + tuning

(*  Title:      Pure/ML-Systems/pp_dummy.ML

Dummy setup for toplevel pretty printing.
*)

fun ml_pretty _ = raise Fail "ml_pretty dummy";
fun pretty_ml _ = raise Fail "pretty_ml dummy";

structure PolyML =
struct
  fun addPrettyPrinter _ = ();
  fun prettyRepresentation _ =
    raise Fail "PolyML.prettyRepresentation dummy";
  open PolyML;
end;