improved output;
authorwenzelm
Sat May 29 15:00:52 2004 +0200 (2004-05-29 ago)
changeset 14824336ade035a34
parent 14823 ebb8499d0fd2
child 14825 8cdf5a813cec
improved output;
src/Pure/axclass.ML
src/Pure/drule.ML
     1.1 --- a/src/Pure/axclass.ML	Sat May 29 15:00:25 2004 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sat May 29 15:00:52 2004 +0200
     1.3 @@ -349,11 +349,11 @@
     1.4      handle ERROR => error ("The error(s) above occurred while trying to prove " ^
     1.5       quote (str_of sign prop))) |> Drule.standard;
     1.6  
     1.7 -val prove_subclass =
     1.8 -  prove mk_classrel (fn sg => fn c1_c2 => Sign.str_of_classrel sg c1_c2);
     1.9 +val prove_subclass = prove mk_classrel (fn sg => fn (c1, c2) =>
    1.10 +  Pretty.string_of_classrel (Sign.pp sg) [c1, c2]);
    1.11  
    1.12 -val prove_arity =
    1.13 -  prove mk_arity (fn sg => fn (t, Ss, c) => Sign.str_of_arity sg (t, Ss, [c]));
    1.14 +val prove_arity = prove mk_arity (fn sg => fn (t, Ss, c) =>
    1.15 +  Pretty.string_of_arity (Sign.pp sg) (t, Ss, [c]));
    1.16  
    1.17  
    1.18  
    1.19 @@ -363,14 +363,14 @@
    1.20  
    1.21  fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c);
    1.22  
    1.23 -fun test_classrel sg cc = (Type.add_classrel [cc] (Sign.tsig_of sg); cc);
    1.24 +fun test_classrel sg cc = (Type.add_classrel (Sign.pp sg) [cc] (Sign.tsig_of sg); cc);
    1.25  fun cert_classrel sg = test_classrel sg o Library.pairself (Sign.certify_class sg);
    1.26  fun read_classrel sg = test_classrel sg o Library.pairself (read_class sg);
    1.27  
    1.28 -fun test_arity sg ar = (Type.add_arities [ar] (Sign.tsig_of sg); ar);
    1.29 +fun test_arity sg ar = (Type.add_arities (Sign.pp sg) [ar] (Sign.tsig_of sg); ar);
    1.30  
    1.31  fun prep_arity prep_tycon prep_sort prep_x sg (t, Ss, x) =
    1.32 -  test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep_x sg x);  
    1.33 +  test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep_x sg x);
    1.34  
    1.35  val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
    1.36  val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
    1.37 @@ -381,10 +381,10 @@
    1.38  fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy =
    1.39    let
    1.40      val sign = Theory.sign_of thy;
    1.41 -    val c1_c2 = prep_classrel sign raw_c1_c2;
    1.42 +    val (c1, c2) = prep_classrel sign raw_c1_c2;
    1.43    in
    1.44 -    message ("Proving class inclusion " ^ quote (Sign.str_of_classrel sign c1_c2) ^ " ...");
    1.45 -    thy |> add_classrel_thms [prove_subclass sign c1_c2 (witnesses thy names thms) usr_tac]
    1.46 +    message ("Proving class inclusion " ^ quote (Sign.string_of_classrel sign [c1, c2]) ^ " ...");
    1.47 +    thy |> add_classrel_thms [prove_subclass sign (c1, c2) (witnesses thy names thms) usr_tac]
    1.48    end;
    1.49  
    1.50  fun ext_inst_arity prep_arity (raw_t, raw_Ss, raw_cs) names thms usr_tac thy =
    1.51 @@ -394,7 +394,7 @@
    1.52      val wthms = witnesses thy names thms;
    1.53      fun prove c =
    1.54       (message ("Proving type arity " ^
    1.55 -        quote (Sign.str_of_arity sign (t, Ss, [c])) ^ " ...");
    1.56 +        quote (Sign.string_of_arity sign (t, Ss, [c])) ^ " ...");
    1.57          prove_arity sign (t, Ss, c) wthms usr_tac);
    1.58    in add_arity_thms (map prove cs) thy end;
    1.59  
     2.1 --- a/src/Pure/drule.ML	Sat May 29 15:00:25 2004 +0200
     2.2 +++ b/src/Pure/drule.ML	Sat May 29 15:00:52 2004 +0200
     2.3 @@ -297,7 +297,7 @@
     2.4  (*Strip extraneous shyps as far as possible*)
     2.5  fun strip_shyps_warning thm =
     2.6    let
     2.7 -    val str_of_sort = Sign.str_of_sort (Thm.sign_of_thm thm);
     2.8 +    val str_of_sort = Pretty.str_of o Sign.pretty_sort (Thm.sign_of_thm thm);
     2.9      val thm' = Thm.strip_shyps thm;
    2.10      val xshyps = Thm.extra_shyps thm';
    2.11    in