src/Pure/display.ML
changeset 16290 e661e37a4d50
parent 16158 2c3565b74b7a
child 16334 b773132e3715
     1.1 --- a/src/Pure/display.ML	Sun Jun 05 23:07:27 2005 +0200
     1.2 +++ b/src/Pure/display.ML	Sun Jun 05 23:07:28 2005 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4  
     1.5  fun pretty_thm_aux pp quote th =
     1.6    let
     1.7 -    val {hyps, tpairs, prop, der = (ora, _), ...} = rep_thm th;
     1.8 +    val {hyps, tpairs, prop, der = (ora, _), ...} = Thm.rep_thm th;
     1.9      val xshyps = Thm.extra_shyps th;
    1.10      val (_, tags) = Thm.get_name_tags th;
    1.11  
    1.12 @@ -182,7 +182,7 @@
    1.13      fun prt_sort S = Sign.pretty_sort sg S;
    1.14      fun prt_arity t (c, Ss) = Sign.pretty_arity sg (t, Ss, [c]);
    1.15      fun prt_typ ty = Pretty.quote (Sign.pretty_typ sg ty);
    1.16 -    val prt_typ_no_tvars = prt_typ o #1 o Type.freeze_thaw_type;
    1.17 +    val prt_typ_no_tvars = prt_typ o Type.freeze_type;
    1.18      fun prt_term t = Pretty.quote (Sign.pretty_term sg t);
    1.19  
    1.20      fun pretty_classrel (c, []) = prt_cls c
    1.21 @@ -223,8 +223,7 @@
    1.22      fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
    1.23  
    1.24  
    1.25 -    val {sign = _, const_deps = const_deps,  axioms, oracles,
    1.26 -      parents = _, ancestors = _} = Theory.rep_theory thy;
    1.27 +    val {sign = _, defs, axioms, oracles, parents = _, ancestors = _} = Theory.rep_theory thy;
    1.28      val {self = _, tsig, consts, naming, spaces, data} = Sign.rep_sg sg;
    1.29      val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
    1.30  
    1.31 @@ -232,7 +231,7 @@
    1.32      val tdecls = Symtab.dest types |> map (fn (t, (d, _)) =>
    1.33        (Sign.extern sg Sign.typeK t, (t, d))) |> Library.sort_wrt #1 |> map #2;
    1.34      val cnsts = Sign.extern_table sg Sign.constK consts;
    1.35 -    val finals = Sign.extern_table sg Sign.constK (Defs.finals const_deps)
    1.36 +    val finals = Sign.extern_table sg Sign.constK (Defs.finals defs);
    1.37      val axms = Sign.extern_table sg Theory.axiomK axioms;
    1.38      val oras = Sign.extern_table sg Theory.oracleK oracles;
    1.39    in
    1.40 @@ -326,7 +325,7 @@
    1.41      val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
    1.42  
    1.43  
    1.44 -    val {prop, tpairs, ...} = rep_thm state;
    1.45 +    val {prop, tpairs, ...} = Thm.rep_thm state;
    1.46      val (As, B) = Logic.strip_horn prop;
    1.47      val ngoals = length As;
    1.48