pretty/print functions with context;
authorwenzelm
Mon Nov 05 20:59:35 2001 +0100 (2001-11-05)
changeset 12055a9c44895cc8c
parent 12054 a96c9563d568
child 12056 5b5ed7eec3a8
pretty/print functions with context;
src/Pure/Isar/calculation.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_output.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/method.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/skip_proof.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Mon Nov 05 20:58:28 2001 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Mon Nov 05 20:59:35 2001 +0100
     1.3 @@ -14,10 +14,12 @@
     1.4    val trans_del_global: theory attribute
     1.5    val trans_add_local: Proof.context attribute
     1.6    val trans_del_local: Proof.context attribute
     1.7 -  val also: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
     1.8 -  val finally: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
     1.9 -  val moreover: (thm list -> unit) -> Proof.state -> Proof.state
    1.10 -  val ultimately: (thm list -> unit) -> Proof.state -> Proof.state
    1.11 +  val also: thm list option -> (Proof.context -> thm list -> unit)
    1.12 +    -> Proof.state -> Proof.state Seq.seq
    1.13 +  val finally: thm list option -> (Proof.context -> thm list -> unit)
    1.14 +    -> Proof.state -> Proof.state Seq.seq
    1.15 +  val moreover: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
    1.16 +  val ultimately: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
    1.17    val setup: (theory -> theory) list
    1.18  end;
    1.19  
    1.20 @@ -28,8 +30,8 @@
    1.21  
    1.22  (* theory data kind 'Isar/calculation' *)
    1.23  
    1.24 -fun print_rules sg rs = Pretty.writeln (Pretty.big_list "transitivity rules:"
    1.25 -  (map (Display.pretty_thm_sg sg) (NetRules.rules rs)));
    1.26 +fun print_rules prt x rs =
    1.27 +  Pretty.writeln (Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules rs)));
    1.28  
    1.29  structure GlobalCalculationArgs =
    1.30  struct
    1.31 @@ -40,7 +42,7 @@
    1.32    val copy = I;
    1.33    val prep_ext = I;
    1.34    val merge = NetRules.merge;
    1.35 -  val print = print_rules;
    1.36 +  val print = print_rules Display.pretty_thm_sg;
    1.37  end;
    1.38  
    1.39  structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
    1.40 @@ -55,7 +57,7 @@
    1.41    type T = thm NetRules.T * (thm list * int) option;
    1.42  
    1.43    fun init thy = (GlobalCalculation.get thy, None);
    1.44 -  fun print ctxt (rs, _) = print_rules (ProofContext.sign_of ctxt) rs;
    1.45 +  fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
    1.46  end;
    1.47  
    1.48  structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
    1.49 @@ -143,7 +145,8 @@
    1.50    in
    1.51      err_if state (initial andalso final) "No calculation yet";
    1.52      err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
    1.53 -    calculations |> Seq.map (fn calc => (print calc; state |> maintain_calculation final calc))
    1.54 +    calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc;
    1.55 +        state |> maintain_calculation final calc))
    1.56    end;
    1.57  
    1.58  fun also print = calculate false print;
    1.59 @@ -162,7 +165,7 @@
    1.60      val calc = thms @ facts;
    1.61    in
    1.62      err_if state (initial andalso final) "No calculation yet";
    1.63 -    print calc;
    1.64 +    print (Proof.context_of state) calc;
    1.65      state |> maintain_calculation final calc
    1.66    end;
    1.67  
     2.1 --- a/src/Pure/Isar/induct_attrib.ML	Mon Nov 05 20:58:28 2001 +0100
     2.2 +++ b/src/Pure/Isar/induct_attrib.ML	Mon Nov 05 20:59:35 2001 +0100
     2.3 @@ -88,9 +88,15 @@
     2.4  
     2.5  fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
     2.6  
     2.7 -fun print_rules kind sg rs =
     2.8 +fun print_rules prt kind x rs =
     2.9    let val thms = map snd (NetRules.rules rs)
    2.10 -  in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end;
    2.11 +  in Pretty.writeln (Pretty.big_list kind (map (prt x) thms)) end;
    2.12 +
    2.13 +fun print_all_rules prt x ((casesT, casesS), (inductT, inductS)) =
    2.14 + (print_rules prt "induct type:" x inductT;
    2.15 +  print_rules prt "induct set:" x inductS;
    2.16 +  print_rules prt "cases type:" x casesT;
    2.17 +  print_rules prt "cases set:" x casesS);
    2.18  
    2.19  
    2.20  (* theory data kind 'Isar/induction' *)
    2.21 @@ -110,11 +116,7 @@
    2.22      ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
    2.23        (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
    2.24  
    2.25 -  fun print sg ((casesT, casesS), (inductT, inductS)) =
    2.26 -    (print_rules "induct type:" sg inductT;
    2.27 -      print_rules "induct set:" sg inductS;
    2.28 -      print_rules "cases type:" sg casesT;
    2.29 -      print_rules "cases set:" sg casesS);
    2.30 +  val print = print_all_rules Display.pretty_thm_sg;
    2.31  
    2.32    fun dest ((casesT, casesS), (inductT, inductS)) =
    2.33      {type_cases = NetRules.rules casesT,
    2.34 @@ -136,7 +138,7 @@
    2.35    type T = GlobalInductArgs.T;
    2.36  
    2.37    fun init thy = GlobalInduct.get thy;
    2.38 -  fun print x = GlobalInductArgs.print (ProofContext.sign_of x);
    2.39 +  val print = print_all_rules ProofContext.pretty_thm;
    2.40  end;
    2.41  
    2.42  structure LocalInduct = ProofDataFun(LocalInductArgs);
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Nov 05 20:58:28 2001 +0100
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Nov 05 20:59:35 2001 +0100
     3.3 @@ -218,7 +218,7 @@
     3.4  
     3.5  val print_lthms = Toplevel.unknown_proof o Toplevel.keep (fn state =>
     3.6    ProofContext.setmp_verbose
     3.7 -    ProofContext.print_thms (Proof.context_of (Toplevel.proof_of state)));
     3.8 +    ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
     3.9  
    3.10  val print_cases = Toplevel.unknown_proof o Toplevel.keep (fn state =>
    3.11    ProofContext.setmp_verbose
    3.12 @@ -228,34 +228,37 @@
    3.13  (* print theorems / types / terms / props *)
    3.14  
    3.15  fun string_of_thms state ms args = with_modes ms (fn () =>
    3.16 -  Pretty.string_of (Proof.pretty_thms (IsarThy.get_thmss args state)));
    3.17 +  Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state)
    3.18 +    (IsarThy.get_thmss args state)));
    3.19  
    3.20  fun string_of_prfs full state ms args = with_modes ms (fn () =>
    3.21 -  Pretty.string_of (Pretty.chunks
    3.22 +  Pretty.string_of (Pretty.chunks    (* FIXME context syntax!? *)
    3.23      (map (ProofSyntax.pretty_proof_of full) (IsarThy.get_thmss args state))));
    3.24  
    3.25  fun string_of_prop state ms s =
    3.26    let
    3.27 -    val sign = Proof.sign_of state;
    3.28 -    val prop = ProofContext.read_prop (Proof.context_of state) s;
    3.29 -  in with_modes ms (fn () => Pretty.string_of (Pretty.quote (Sign.pretty_term sign prop))) end;
    3.30 +    val ctxt = Proof.context_of state;
    3.31 +    val prop = ProofContext.read_prop ctxt s;
    3.32 +  in
    3.33 +    with_modes ms (fn () => Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)))
    3.34 +  end;
    3.35  
    3.36  fun string_of_term state ms s =
    3.37    let
    3.38 -    val sign = Proof.sign_of state;
    3.39 -    val t = ProofContext.read_term (Proof.context_of state) s;
    3.40 +    val ctxt = Proof.context_of state;
    3.41 +    val t = ProofContext.read_term ctxt s;
    3.42      val T = Term.type_of t;
    3.43    in
    3.44      with_modes ms (fn () => Pretty.string_of
    3.45 -      (Pretty.block [Pretty.quote (Sign.pretty_term sign t), Pretty.fbrk,
    3.46 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ sign T)]))
    3.47 +      (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
    3.48 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)]))
    3.49    end;
    3.50  
    3.51  fun string_of_type state ms s =
    3.52    let
    3.53 -    val sign = Proof.sign_of state;
    3.54 -    val T = ProofContext.read_typ (Proof.context_of state) s;
    3.55 -  in with_modes ms (fn () => Pretty.string_of (Pretty.quote (Sign.pretty_typ sign T))) end;
    3.56 +    val ctxt = Proof.context_of state;
    3.57 +    val T = ProofContext.read_typ ctxt s;
    3.58 +  in with_modes ms (fn () => Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T))) end;
    3.59  
    3.60  fun print_item string_of (x, y) = Toplevel.keep (fn state =>
    3.61    writeln (string_of (Toplevel.enter_forward_proof state) x y));
     4.1 --- a/src/Pure/Isar/isar_output.ML	Mon Nov 05 20:58:28 2001 +0100
     4.2 +++ b/src/Pure/Isar/isar_output.ML	Mon Nov 05 20:59:35 2001 +0100
     4.3 @@ -292,21 +292,17 @@
     4.4  val pretty_source =
     4.5    pretty_text o space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
     4.6  
     4.7 -fun pretty_typ ctxt T =
     4.8 -  Sign.pretty_typ (ProofContext.sign_of ctxt) T;
     4.9 +fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
    4.10  
    4.11 -fun pretty_term ctxt t =
    4.12 -  Sign.pretty_term (ProofContext.sign_of ctxt) (ProofContext.extern_skolem ctxt t);
    4.13 -
    4.14 -fun pretty_thm ctxt thms =
    4.15 +fun pretty_thms ctxt thms =
    4.16    Pretty.chunks (map (pretty_term ctxt o #prop o Thm.rep_thm) thms);
    4.17  
    4.18 -fun pretty_prf full ctxt thms =
    4.19 +fun pretty_prf full ctxt thms =    (* FIXME context syntax!? *)
    4.20    Pretty.chunks (map (ProofSyntax.pretty_proof_of full) thms);
    4.21  
    4.22  fun output_with pretty src ctxt x =
    4.23    let
    4.24 -    val prt = pretty ctxt x;      (*always pretty!*)
    4.25 +    val prt = pretty ctxt x;      (*always pretty in order to catch errors!*)
    4.26      val prt' = if ! source then pretty_source src else prt;
    4.27    in cond_display (cond_quote prt') end;
    4.28  
    4.29 @@ -316,12 +312,12 @@
    4.30  
    4.31  val _ = add_commands
    4.32   [("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
    4.33 -  ("thm", args Attrib.local_thmss (output_with pretty_thm)),
    4.34 +  ("thm", args Attrib.local_thmss (output_with pretty_thms)),
    4.35    ("prf", args Attrib.local_thmss (output_with (pretty_prf false))),
    4.36    ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true))),
    4.37    ("prop", args Args.local_prop (output_with pretty_term)),
    4.38    ("term", args Args.local_term (output_with pretty_term)),
    4.39 -  ("typ", args Args.local_typ_no_norm (output_with pretty_typ)),
    4.40 +  ("typ", args Args.local_typ_no_norm (output_with ProofContext.pretty_typ)),
    4.41    ("goals", output_goals true),
    4.42    ("subgoals", output_goals false)];
    4.43  
     5.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Nov 05 20:58:28 2001 +0100
     5.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Nov 05 20:59:35 2001 +0100
     5.3 @@ -360,21 +360,21 @@
     5.4  
     5.5  local
     5.6  
     5.7 -fun pretty_result {kind, name, thm} =
     5.8 +fun pretty_result ctxt {kind, name, thm} =
     5.9    Pretty.block [Pretty.str (kind ^ (if name = "" then "" else " " ^ name) ^ ":"),
    5.10 -    Pretty.fbrk, Proof.pretty_thm thm];
    5.11 +    Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
    5.12  
    5.13 -fun pretty_rule s thm =
    5.14 +fun pretty_rule s ctxt thm =
    5.15    Pretty.block [Pretty.str (s ^ " to solve goal by exported rule:"),
    5.16 -    Pretty.fbrk, Proof.pretty_thm thm];
    5.17 +    Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
    5.18  
    5.19  in
    5.20  
    5.21 -val print_result = Pretty.writeln o pretty_result;
    5.22 +val print_result = Pretty.writeln oo pretty_result;
    5.23  
    5.24  fun cond_print_result_rule int =
    5.25 -  if int then (print_result, priority o Pretty.string_of o pretty_rule "Attempt")
    5.26 -  else (K (), K ());
    5.27 +  if int then (print_result, priority oo (Pretty.string_of oo pretty_rule "Attempt"))
    5.28 +  else (K (K ()), K (K ()));
    5.29  
    5.30  fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);
    5.31  
    5.32 @@ -386,10 +386,11 @@
    5.33            (["Problem! Local statement will fail to solve any pending goal"] @
    5.34            (case exn of None => [] | Some e => [Toplevel.exn_message e]) @
    5.35            (case ! rule of None => [] | Some thm =>
    5.36 -            [Pretty.string_of (pretty_rule "Failed attempt" thm)]))
    5.37 +            [Pretty.string_of (pretty_rule "Failed attempt" (Proof.context_of state) thm)]))
    5.38            |> cat_lines |> warning;
    5.39          val check =
    5.40 -          (fn () => Seq.pull (SkipProof.local_skip_proof (K (), fn thm => rule := Some thm) state))
    5.41 +          (fn () => Seq.pull (SkipProof.local_skip_proof (K (K ()),
    5.42 +            fn _ => fn thm => rule := Some thm) state))
    5.43            |> Library.setmp quick_and_dirty true
    5.44            |> Library.setmp proofs 0
    5.45            |> Library.transform_error;
    5.46 @@ -507,7 +508,8 @@
    5.47      val (thy, res as {kind, name, thm}) = finish state;
    5.48    in
    5.49      if kind = "" orelse kind = Drule.internalK then ()
    5.50 -    else (print_result res; Context.setmp (Some thy) (Present.result kind name) thm);
    5.51 +    else (print_result (Proof.context_of state) res;
    5.52 +      Context.setmp (Some thy) (Present.result kind name) thm);
    5.53      thy
    5.54    end);
    5.55  
    5.56 @@ -535,8 +537,9 @@
    5.57  
    5.58  local
    5.59  
    5.60 -fun cond_print_calc int thms =
    5.61 -  if int then Pretty.writeln (Pretty.big_list "calculation:" (map Proof.pretty_thm thms))
    5.62 +fun cond_print_calc int ctxt thms =
    5.63 +  if int then
    5.64 +    Pretty.writeln (Pretty.big_list "calculation:" (map (ProofContext.pretty_thm ctxt) thms))
    5.65    else ();
    5.66  
    5.67  fun proof''' f = Toplevel.proof' (f o cond_print_calc);
     6.1 --- a/src/Pure/Isar/method.ML	Mon Nov 05 20:58:28 2001 +0100
     6.2 +++ b/src/Pure/Isar/method.ML	Mon Nov 05 20:59:35 2001 +0100
     6.3 @@ -16,7 +16,7 @@
     6.4  signature METHOD =
     6.5  sig
     6.6    include BASIC_METHOD
     6.7 -  val trace: thm list -> unit
     6.8 +  val trace: Proof.context -> thm list -> unit
     6.9    val print_global_rules: theory -> unit
    6.10    val print_local_rules: Proof.context -> unit
    6.11    val dest_global: theory attribute
    6.12 @@ -99,17 +99,17 @@
    6.13    val refine_end: text -> Proof.state -> Proof.state Seq.seq
    6.14    val proof: text option -> Proof.state -> Proof.state Seq.seq
    6.15    val local_qed: bool -> text option
    6.16 -    -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    6.17 -    -> Proof.state -> Proof.state Seq.seq
    6.18 +    -> (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
    6.19 +      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
    6.20    val local_terminal_proof: text * text option
    6.21 -    -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    6.22 -    -> Proof.state -> Proof.state Seq.seq
    6.23 -  val local_default_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    6.24 -    -> Proof.state -> Proof.state Seq.seq
    6.25 -  val local_immediate_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    6.26 -    -> Proof.state -> Proof.state Seq.seq
    6.27 -  val local_done_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    6.28 -    -> Proof.state -> Proof.state Seq.seq
    6.29 +    -> (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
    6.30 +      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
    6.31 +  val local_default_proof: (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
    6.32 +    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
    6.33 +  val local_immediate_proof: (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
    6.34 +    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
    6.35 +  val local_done_proof: (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
    6.36 +    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
    6.37    val global_qed: bool -> text option
    6.38      -> Proof.state -> theory * {kind: string, name: string, thm: thm}
    6.39    val global_terminal_proof: text * text option
    6.40 @@ -132,9 +132,9 @@
    6.41  
    6.42  val trace_rules = ref false;
    6.43  
    6.44 -fun trace rules =
    6.45 +fun trace ctxt rules =
    6.46    if not (! trace_rules) orelse null rules then ()
    6.47 -  else Pretty.writeln (Pretty.big_list "rules:" (map Display.pretty_thm rules));
    6.48 +  else Pretty.writeln (Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules));
    6.49  
    6.50  
    6.51  
    6.52 @@ -153,12 +153,11 @@
    6.53    | kind_name 3 = "elimination rules (elim)"
    6.54    | kind_name _ = "unknown";
    6.55  
    6.56 -fun prt_rules sg (k, rs) =
    6.57 -  Pretty.writeln (Pretty.big_list (kind_name k ^ ":")
    6.58 -    (map (Display.pretty_thm_sg sg) (NetRules.rules rs)));
    6.59 +fun prt_rules prt x (k, rs) =
    6.60 +  Pretty.writeln (Pretty.big_list (kind_name k ^ ":") (map (prt x) (NetRules.rules rs)));
    6.61  
    6.62  in
    6.63 -  fun print_rules sg rules = seq (prt_rules sg) (0 upto length rules - 1 ~~ rules);
    6.64 +  fun print_rules prt x rules = seq (prt_rules prt x) (0 upto length rules - 1 ~~ rules);
    6.65  end;
    6.66  
    6.67  
    6.68 @@ -173,7 +172,7 @@
    6.69    val copy = I;
    6.70    val prep_ext = I;
    6.71    fun merge x = map2 NetRules.merge x;
    6.72 -  val print = print_rules;
    6.73 +  val print = print_rules Display.pretty_thm_sg;
    6.74  end;
    6.75  
    6.76  structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
    6.77 @@ -187,7 +186,7 @@
    6.78    val name = GlobalRulesArgs.name;
    6.79    type T = GlobalRulesArgs.T;
    6.80    val init = GlobalRules.get;
    6.81 -  val print = print_rules o ProofContext.sign_of;
    6.82 +  val print = print_rules ProofContext.pretty_thm;
    6.83  end;
    6.84  
    6.85  structure LocalRules = ProofDataFun(LocalRulesArgs);
    6.86 @@ -352,7 +351,7 @@
    6.87        if not (null arg_rules) then arg_rules
    6.88        else find_erules facts (get elim_bangK) @ find_erules facts (get elimK) @
    6.89          find_rules goal (get intro_bangK) @ find_rules goal (get introK);
    6.90 -  in trace rules; tac rules facts i end);
    6.91 +  in trace ctxt rules; tac rules facts i end);
    6.92  
    6.93  fun meth tac x = METHOD (HEADGOAL o tac x);
    6.94  fun meth' tac x y = METHOD (HEADGOAL o tac x y);
     7.1 --- a/src/Pure/Isar/obtain.ML	Mon Nov 05 20:58:28 2001 +0100
     7.2 +++ b/src/Pure/Isar/obtain.ML	Mon Nov 05 20:59:35 2001 +0100
     7.3 @@ -50,7 +50,7 @@
     7.4    in
     7.5      if not (null bads) then
     7.6        raise Proof.STATE ("Conclusion contains obtained parameters: " ^
     7.7 -        space_implode " " (map (Sign.string_of_term sign) bads), state)
     7.8 +        space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state)
     7.9      else if not (ObjectLogic.is_judgment sign (Logic.strip_assums_concl prop)) then
    7.10        raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
    7.11      else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
     8.1 --- a/src/Pure/Isar/proof.ML	Mon Nov 05 20:58:28 2001 +0100
     8.2 +++ b/src/Pure/Isar/proof.ML	Mon Nov 05 20:59:35 2001 +0100
     8.3 @@ -37,9 +37,6 @@
     8.4    val assert_backward: state -> state
     8.5    val assert_no_chain: state -> state
     8.6    val enter_forward: state -> state
     8.7 -  val show_hyps: bool ref
     8.8 -  val pretty_thm: thm -> Pretty.T
     8.9 -  val pretty_thms: thm list -> Pretty.T
    8.10    val verbose: bool ref
    8.11    val print_state: int -> state -> unit
    8.12    val pretty_goals: bool -> state -> Pretty.T list
    8.13 @@ -95,7 +92,8 @@
    8.14      -> term * (term list * term list) -> state -> state
    8.15    val at_bottom: state -> bool
    8.16    val local_qed: (state -> state Seq.seq)
    8.17 -    -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) -> state -> state Seq.seq
    8.18 +    -> (context -> {kind: string, name: string, thm: thm} -> unit) *
    8.19 +      (context -> thm -> unit) -> state -> state Seq.seq
    8.20    val global_qed: (state -> state Seq.seq) -> state
    8.21      -> (theory * {kind: string, name: string, thm: thm}) Seq.seq
    8.22    val begin_block: state -> state
    8.23 @@ -203,7 +201,6 @@
    8.24  val put_thms = map_context o ProofContext.put_thms;
    8.25  val put_thmss = map_context o ProofContext.put_thmss;
    8.26  val reset_thms = map_context o ProofContext.reset_thms;
    8.27 -val assumptions = ProofContext.assumptions o context_of;
    8.28  val get_case = ProofContext.get_case o context_of;
    8.29  
    8.30  
    8.31 @@ -308,18 +305,11 @@
    8.32  
    8.33  (** print_state **)
    8.34  
    8.35 -val show_hyps = ProofContext.show_hyps;
    8.36 -val pretty_thm = ProofContext.pretty_thm;
    8.37 -
    8.38 -fun pretty_thms [th] = pretty_thm th
    8.39 -  | pretty_thms ths = Pretty.blk (0, Pretty.fbreaks (map pretty_thm ths));
    8.40 -
    8.41 -
    8.42  val verbose = ProofContext.verbose;
    8.43  
    8.44 -fun pretty_facts _ None = []
    8.45 -  | pretty_facts s (Some ths) =
    8.46 -      [Pretty.big_list (s ^ "this:") (map pretty_thm ths), Pretty.str ""];
    8.47 +fun pretty_facts _ _ None = []
    8.48 +  | pretty_facts s ctxt (Some ths) =
    8.49 +      [Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""];
    8.50  
    8.51  fun print_state nr (state as State (Node {context, facts, mode, goal = _}, nodes)) =
    8.52    let
    8.53 @@ -334,7 +324,7 @@
    8.54        | subgoals n = ", " ^ string_of_int n ^ " subgoals";
    8.55        
    8.56      fun pretty_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) =
    8.57 -      pretty_facts "using "
    8.58 +      pretty_facts "using " context
    8.59          (if mode <> Backward orelse null goal_facts then None else Some goal_facts) @
    8.60        [Pretty.str ("goal (" ^ kind_name (sign_of state) kind ^
    8.61            (if name = "" then "" else " " ^ name) ^
    8.62 @@ -343,7 +333,7 @@
    8.63  
    8.64      val ctxt_prts =
    8.65        if ! verbose orelse mode = Forward then ProofContext.pretty_context context
    8.66 -      else if mode = Backward then ProofContext.pretty_prems context
    8.67 +      else if mode = Backward then ProofContext.pretty_asms context
    8.68        else [];
    8.69  
    8.70      val prts =
    8.71 @@ -352,8 +342,8 @@
    8.72          else "")), Pretty.str ""] @
    8.73       (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @
    8.74       (if ! verbose orelse mode = Forward then
    8.75 -       (pretty_facts "" facts @ pretty_goal (find_goal state))
    8.76 -      else if mode = ForwardChain then pretty_facts "picking " facts
    8.77 +       (pretty_facts "" context facts @ pretty_goal (find_goal state))
    8.78 +      else if mode = ForwardChain then pretty_facts "picking " context facts
    8.79        else pretty_goal (find_goal state))
    8.80    in Pretty.writeln (Pretty.chunks prts) end;
    8.81  
    8.82 @@ -424,7 +414,7 @@
    8.83      val exp_tac = ProofContext.export true inner outer;
    8.84      fun exp_rule rule =
    8.85        let
    8.86 -        val _ = print_rule rule;
    8.87 +        val _ = print_rule outer rule;
    8.88          val thmq = FINDGOAL (refine_tac rule) thm;
    8.89        in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end;
    8.90    in raw_rule |> exp_tac |> (Seq.flat o Seq.map exp_rule) end;
    8.91 @@ -455,13 +445,13 @@
    8.92      val {hyps, prop, sign, ...} = Thm.rep_thm thm;
    8.93      val tsig = Sign.tsig_of sign;
    8.94  
    8.95 -    val casms = flat (map #1 (assumptions state));
    8.96 +    val casms = flat (map #1 (ProofContext.assumptions_of (context_of state)));
    8.97      val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms);
    8.98    in
    8.99 -    if not (null bad_hyps) then
   8.100 -      err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
   8.101 +    if not (null bad_hyps) then err ("Additional hypotheses:\n" ^
   8.102 +        cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps))
   8.103      else if not (Pattern.matches (Sign.tsig_of (sign_of state)) (t, prop)) then
   8.104 -      err ("Proved a different theorem: " ^ Sign.string_of_term sign prop)
   8.105 +      err ("Proved a different theorem: " ^ ProofContext.string_of_term ctxt prop)
   8.106      else thm
   8.107    end;
   8.108  
   8.109 @@ -608,7 +598,7 @@
   8.110        commas (map (Syntax.string_of_vname o #1) tvars), state);
   8.111      if null vars then ()
   8.112      else warning ("Goal statement contains unbound schematic variable(s): " ^
   8.113 -      commas (map (Sign.string_of_term (sign_of state)) vars));
   8.114 +      commas (map (ProofContext.string_of_term (context_of state')) vars));
   8.115      state'
   8.116      |> map_context (autofix prop)
   8.117      |> put_goal (Some (((kind, name, prop), ([], goal)), after_qed o map_context gen_binds))
   8.118 @@ -700,7 +690,7 @@
   8.119        | Have atts => (atts, Seq.single)
   8.120        | _ => err_malformed "finish_local" state);
   8.121    in
   8.122 -    print_result {kind = kind_name (sign_of state) kind, name = name, thm = result};
   8.123 +    print_result goal_ctxt {kind = kind_name (sign_of state) kind, name = name, thm = result};
   8.124      outer_state
   8.125      |> auto_bind_facts name [ProofContext.generalize goal_ctxt outer_ctxt t]
   8.126      |> (fn st => Seq.map (fn res =>
     9.1 --- a/src/Pure/Isar/skip_proof.ML	Mon Nov 05 20:58:28 2001 +0100
     9.2 +++ b/src/Pure/Isar/skip_proof.ML	Mon Nov 05 20:59:35 2001 +0100
     9.3 @@ -12,8 +12,8 @@
     9.4    val make_thm: theory -> term -> thm
     9.5    val cheat_tac: theory -> tactic
     9.6    val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
     9.7 -  val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
     9.8 -    -> Proof.state -> Proof.state Seq.seq
     9.9 +  val local_skip_proof: (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
    9.10 +    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
    9.11    val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    9.12    val setup: (theory -> theory) list
    9.13  end;