src/Pure/Isar/proof_context.ML
changeset 7575 e1e2d07287d8
parent 7557 1b977741f530
child 7606 7905a74eb068
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Sep 22 20:59:22 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Sep 22 21:02:32 1999 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    val verbose: bool ref
     1.5    val print_binds: context -> unit
     1.6    val print_thms: context -> unit
     1.7 +  val strings_of_prems: context -> string list
     1.8    val strings_of_context: context -> string list
     1.9    val print_proof_data: theory -> unit
    1.10    val init: theory -> context
    1.11 @@ -112,7 +113,10 @@
    1.12  (** print context information **)
    1.13  
    1.14  val show_hyps = ref false;
    1.15 -fun pretty_thm th = setmp Display.show_hyps (! show_hyps) Display.pretty_thm th;
    1.16 +
    1.17 +fun pretty_thm thm =
    1.18 +  if ! show_hyps then setmp Display.show_hyps true Display.pretty_thm_no_quote thm
    1.19 +  else Display.pretty_cterm (#prop (Thm.crep_thm thm));
    1.20  
    1.21  val verbose = ref false;
    1.22  fun verb f x = if ! verbose then f x else [];
    1.23 @@ -130,13 +134,13 @@
    1.24  
    1.25  (* term bindings *)
    1.26  
    1.27 -fun strings_of_binds (Context {thy, binds, ...}) =
    1.28 +fun strings_of_binds (ctxt as Context {binds, ...}) =
    1.29    let
    1.30 -    val prt_term = Sign.pretty_term (Theory.sign_of thy);
    1.31 +    val prt_term = Sign.pretty_term (sign_of ctxt);
    1.32      fun pretty_bind (xi, (t, T)) = prt_term (Logic.mk_equals (Var (xi, T), t));
    1.33    in
    1.34      if Vartab.is_empty binds andalso not (! verbose) then []
    1.35 -    else [Pretty.string_of (Pretty.big_list "Term bindings:"
    1.36 +    else [Pretty.string_of (Pretty.big_list "term bindings:"
    1.37        (map pretty_bind (Vartab.dest binds)))]
    1.38    end;
    1.39  
    1.40 @@ -146,18 +150,22 @@
    1.41  (* local theorems *)
    1.42  
    1.43  fun strings_of_thms (Context {thms, ...}) =
    1.44 -  strings_of_items pretty_thm "Local theorems:" (Symtab.dest thms);
    1.45 +  strings_of_items pretty_thm "local theorems:" (Symtab.dest thms);
    1.46  
    1.47  val print_thms = seq writeln o strings_of_thms;
    1.48  
    1.49  
    1.50  (* main context *)
    1.51  
    1.52 -fun strings_of_context (ctxt as Context {thy, data = _, asms = (_, (fixes, _)), binds = _,
    1.53 -    thms = _, defs = (types, sorts, maxidx, used)}) =
    1.54 +fun strings_of_prems ctxt =
    1.55 +  (case prems_of ctxt of
    1.56 +    [] => []
    1.57 +  | prems => [Pretty.string_of (Pretty.big_list "prems:" (map pretty_thm prems))]);
    1.58 +
    1.59 +fun strings_of_context (ctxt as Context {asms = (_, (fixes, _)),
    1.60 +    defs = (types, sorts, maxidx, used), ...}) =
    1.61    let
    1.62 -    val sign = Theory.sign_of thy;
    1.63 -    val prems = prems_of ctxt;
    1.64 +    val sign = sign_of ctxt;
    1.65  
    1.66      val prt_term = Sign.pretty_term sign;
    1.67      val prt_typ = Sign.pretty_typ sign;
    1.68 @@ -167,7 +175,7 @@
    1.69      val pretty_thy = Pretty.block [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg sign];
    1.70  
    1.71      (*fixes*)
    1.72 -    fun prt_fixes xs = Pretty.block (Pretty.str "Fixed variables:" :: Pretty.brk 1 ::
    1.73 +    fun prt_fixes xs = Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
    1.74        Pretty.commas (map (fn (x, x') => Pretty.str (x ^ " = " ^ x')) xs));
    1.75  
    1.76  
    1.77 @@ -186,17 +194,14 @@
    1.78      val prt_defS = prt_atom prt_varT prt_sort;
    1.79    in
    1.80      verb_string pretty_thy @
    1.81 -    (if null fixes andalso not (! verbose) then []
    1.82 -      else [Pretty.string_of (prt_fixes (rev fixes))]) @
    1.83 -    (if null prems andalso not (! verbose) then []
    1.84 -      else [Pretty.string_of (Pretty.big_list "Assumptions:"
    1.85 -        (map (prt_term o #prop o Thm.rep_thm) prems))]) @
    1.86 +    (if null fixes then [] else [Pretty.string_of (prt_fixes (rev fixes))]) @
    1.87 +    strings_of_prems ctxt @
    1.88      verb strings_of_binds ctxt @
    1.89      verb strings_of_thms ctxt @
    1.90 -    verb_string (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types))) @
    1.91 -    verb_string (Pretty.big_list "Default sorts:" (map prt_defS (Vartab.dest sorts))) @
    1.92 -    verb_string (Pretty.str ("Maxidx: " ^ string_of_int maxidx)) @
    1.93 -    verb_string (Pretty.strs ("Used type variable names:" :: used))
    1.94 +    verb_string (Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
    1.95 +    verb_string (Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) @
    1.96 +    verb_string (Pretty.str ("maxidx: " ^ string_of_int maxidx)) @
    1.97 +    verb_string (Pretty.strs ("used type variable names:" :: used))
    1.98    end;
    1.99  
   1.100  
   1.101 @@ -298,11 +303,8 @@
   1.102  (** prepare types **)
   1.103  
   1.104  fun read_typ (ctxt as Context {defs = (_, sorts, _, _), ...}) s =
   1.105 -  let
   1.106 -    val sign = sign_of ctxt;
   1.107 -    fun def_sort xi = Vartab.lookup (sorts, xi);
   1.108 -  in
   1.109 -    transform_error (Sign.read_typ (sign, def_sort)) s
   1.110 +  let fun def_sort xi = Vartab.lookup (sorts, xi) in
   1.111 +    transform_error (Sign.read_typ (sign_of ctxt, def_sort)) s
   1.112        handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)
   1.113    end;
   1.114  
   1.115 @@ -425,8 +427,6 @@
   1.116  
   1.117  fun gen_read read app is_pat (ctxt as Context {binds, defs = (types, sorts, _, used), ...}) s =
   1.118    let
   1.119 -    val sign = sign_of ctxt;
   1.120 -
   1.121      fun def_type xi =
   1.122        (case Vartab.lookup (types, xi) of
   1.123          None => if is_pat then None else apsome #2 (Vartab.lookup (binds, xi))
   1.124 @@ -434,7 +434,7 @@
   1.125  
   1.126      fun def_sort xi = Vartab.lookup (sorts, xi);
   1.127    in
   1.128 -    (transform_error (read sign (def_type, def_sort, used)) s
   1.129 +    (transform_error (read (sign_of ctxt) (def_type, def_sort, used)) s
   1.130        handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
   1.131        | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
   1.132      |> app (intern_skolem ctxt true)
   1.133 @@ -642,10 +642,9 @@
   1.134  fun gen_assm prepp tac (ctxt, (name, attrs, raw_prop_pats)) =
   1.135    let
   1.136      val (ctxt', props) = foldl_map prepp (ctxt, raw_prop_pats);
   1.137 -    val sign = sign_of ctxt';
   1.138      val Context {defs = (_, _, maxidx, _), ...} = ctxt';
   1.139  
   1.140 -    val cprops = map (Thm.cterm_of sign) props;
   1.141 +    val cprops = map (Thm.cterm_of (sign_of ctxt')) props;
   1.142      val cprops_tac = map (rpair tac) cprops;
   1.143      val asms = map (Drule.forall_elim_vars (maxidx + 1) o Drule.assume_goal) cprops;
   1.144