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;