pretty/print functions with context;

--- a/src/Pure/Isar/calculation.ML	Mon Nov 05 20:58:28 2001 +0100
+++ b/src/Pure/Isar/calculation.ML	Mon Nov 05 20:59:35 2001 +0100
@@ -14,10 +14,12 @@
   val trans_del_global: theory attribute
   val trans_add_local: Proof.context attribute
   val trans_del_local: Proof.context attribute
-  val also: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
-  val finally: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
-  val moreover: (thm list -> unit) -> Proof.state -> Proof.state
-  val ultimately: (thm list -> unit) -> Proof.state -> Proof.state
+  val also: thm list option -> (Proof.context -> thm list -> unit)
+    -> Proof.state -> Proof.state Seq.seq
+  val finally: thm list option -> (Proof.context -> thm list -> unit)
+    -> Proof.state -> Proof.state Seq.seq
+  val moreover: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
+  val ultimately: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
   val setup: (theory -> theory) list
 end;
 
@@ -28,8 +30,8 @@
 
 (* theory data kind 'Isar/calculation' *)
 
-fun print_rules sg rs = Pretty.writeln (Pretty.big_list "transitivity rules:"
-  (map (Display.pretty_thm_sg sg) (NetRules.rules rs)));
+fun print_rules prt x rs =
+  Pretty.writeln (Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules rs)));
 
 structure GlobalCalculationArgs =
 struct
@@ -40,7 +42,7 @@
   val copy = I;
   val prep_ext = I;
   val merge = NetRules.merge;
-  val print = print_rules;
+  val print = print_rules Display.pretty_thm_sg;
 end;
 
 structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
@@ -55,7 +57,7 @@
   type T = thm NetRules.T * (thm list * int) option;
 
   fun init thy = (GlobalCalculation.get thy, None);
-  fun print ctxt (rs, _) = print_rules (ProofContext.sign_of ctxt) rs;
+  fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
 end;
 
 structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
@@ -143,7 +145,8 @@
   in
     err_if state (initial andalso final) "No calculation yet";
     err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
-    calculations |> Seq.map (fn calc => (print calc; state |> maintain_calculation final calc))
+    calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc;
+        state |> maintain_calculation final calc))
   end;
 
 fun also print = calculate false print;
@@ -162,7 +165,7 @@
     val calc = thms @ facts;
   in
     err_if state (initial andalso final) "No calculation yet";
-    print calc;
+    print (Proof.context_of state) calc;
     state |> maintain_calculation final calc
   end;
 

--- a/src/Pure/Isar/induct_attrib.ML	Mon Nov 05 20:58:28 2001 +0100
+++ b/src/Pure/Isar/induct_attrib.ML	Mon Nov 05 20:59:35 2001 +0100
@@ -88,9 +88,15 @@
 
 fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
 
-fun print_rules kind sg rs =
+fun print_rules prt kind x rs =
   let val thms = map snd (NetRules.rules rs)
-  in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end;
+  in Pretty.writeln (Pretty.big_list kind (map (prt x) thms)) end;
+
+fun print_all_rules prt x ((casesT, casesS), (inductT, inductS)) =
+ (print_rules prt "induct type:" x inductT;
+  print_rules prt "induct set:" x inductS;
+  print_rules prt "cases type:" x casesT;
+  print_rules prt "cases set:" x casesS);
 
 
 (* theory data kind 'Isar/induction' *)
@@ -110,11 +116,7 @@
     ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
 
-  fun print sg ((casesT, casesS), (inductT, inductS)) =
-    (print_rules "induct type:" sg inductT;
-      print_rules "induct set:" sg inductS;
-      print_rules "cases type:" sg casesT;
-      print_rules "cases set:" sg casesS);
+  val print = print_all_rules Display.pretty_thm_sg;
 
   fun dest ((casesT, casesS), (inductT, inductS)) =
     {type_cases = NetRules.rules casesT,
@@ -136,7 +138,7 @@
   type T = GlobalInductArgs.T;
 
   fun init thy = GlobalInduct.get thy;
-  fun print x = GlobalInductArgs.print (ProofContext.sign_of x);
+  val print = print_all_rules ProofContext.pretty_thm;
 end;
 
 structure LocalInduct = ProofDataFun(LocalInductArgs);

--- a/src/Pure/Isar/isar_cmd.ML	Mon Nov 05 20:58:28 2001 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Nov 05 20:59:35 2001 +0100
@@ -218,7 +218,7 @@
 
 val print_lthms = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   ProofContext.setmp_verbose
-    ProofContext.print_thms (Proof.context_of (Toplevel.proof_of state)));
+    ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
 
 val print_cases = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   ProofContext.setmp_verbose
@@ -228,34 +228,37 @@
 (* print theorems / types / terms / props *)
 
 fun string_of_thms state ms args = with_modes ms (fn () =>
-  Pretty.string_of (Proof.pretty_thms (IsarThy.get_thmss args state)));
+  Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state)
+    (IsarThy.get_thmss args state)));
 
 fun string_of_prfs full state ms args = with_modes ms (fn () =>
-  Pretty.string_of (Pretty.chunks
+  Pretty.string_of (Pretty.chunks    (* FIXME context syntax!? *)
     (map (ProofSyntax.pretty_proof_of full) (IsarThy.get_thmss args state))));
 
 fun string_of_prop state ms s =
   let
-    val sign = Proof.sign_of state;
-    val prop = ProofContext.read_prop (Proof.context_of state) s;
-  in with_modes ms (fn () => Pretty.string_of (Pretty.quote (Sign.pretty_term sign prop))) end;
+    val ctxt = Proof.context_of state;
+    val prop = ProofContext.read_prop ctxt s;
+  in
+    with_modes ms (fn () => Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)))
+  end;
 
 fun string_of_term state ms s =
   let
-    val sign = Proof.sign_of state;
-    val t = ProofContext.read_term (Proof.context_of state) s;
+    val ctxt = Proof.context_of state;
+    val t = ProofContext.read_term ctxt s;
     val T = Term.type_of t;
   in
     with_modes ms (fn () => Pretty.string_of
-      (Pretty.block [Pretty.quote (Sign.pretty_term sign t), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ sign T)]))
+      (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
+        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)]))
   end;
 
 fun string_of_type state ms s =
   let
-    val sign = Proof.sign_of state;
-    val T = ProofContext.read_typ (Proof.context_of state) s;
-  in with_modes ms (fn () => Pretty.string_of (Pretty.quote (Sign.pretty_typ sign T))) end;
+    val ctxt = Proof.context_of state;
+    val T = ProofContext.read_typ ctxt s;
+  in with_modes ms (fn () => Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T))) end;
 
 fun print_item string_of (x, y) = Toplevel.keep (fn state =>
   writeln (string_of (Toplevel.enter_forward_proof state) x y));

--- a/src/Pure/Isar/isar_output.ML	Mon Nov 05 20:58:28 2001 +0100
+++ b/src/Pure/Isar/isar_output.ML	Mon Nov 05 20:59:35 2001 +0100
@@ -292,21 +292,17 @@
 val pretty_source =
   pretty_text o space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
 
-fun pretty_typ ctxt T =
-  Sign.pretty_typ (ProofContext.sign_of ctxt) T;
+fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
 
-fun pretty_term ctxt t =
-  Sign.pretty_term (ProofContext.sign_of ctxt) (ProofContext.extern_skolem ctxt t);
-
-fun pretty_thm ctxt thms =
+fun pretty_thms ctxt thms =
   Pretty.chunks (map (pretty_term ctxt o #prop o Thm.rep_thm) thms);
 
-fun pretty_prf full ctxt thms =
+fun pretty_prf full ctxt thms =    (* FIXME context syntax!? *)
   Pretty.chunks (map (ProofSyntax.pretty_proof_of full) thms);
 
 fun output_with pretty src ctxt x =
   let
-    val prt = pretty ctxt x;      (*always pretty!*)
+    val prt = pretty ctxt x;      (*always pretty in order to catch errors!*)
     val prt' = if ! source then pretty_source src else prt;
   in cond_display (cond_quote prt') end;
 
@@ -316,12 +312,12 @@
 
 val _ = add_commands
  [("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
-  ("thm", args Attrib.local_thmss (output_with pretty_thm)),
+  ("thm", args Attrib.local_thmss (output_with pretty_thms)),
   ("prf", args Attrib.local_thmss (output_with (pretty_prf false))),
   ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true))),
   ("prop", args Args.local_prop (output_with pretty_term)),
   ("term", args Args.local_term (output_with pretty_term)),
-  ("typ", args Args.local_typ_no_norm (output_with pretty_typ)),
+  ("typ", args Args.local_typ_no_norm (output_with ProofContext.pretty_typ)),
   ("goals", output_goals true),
   ("subgoals", output_goals false)];
 

--- a/src/Pure/Isar/isar_thy.ML	Mon Nov 05 20:58:28 2001 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Mon Nov 05 20:59:35 2001 +0100
@@ -360,21 +360,21 @@
 
 local
 
-fun pretty_result {kind, name, thm} =
+fun pretty_result ctxt {kind, name, thm} =
   Pretty.block [Pretty.str (kind ^ (if name = "" then "" else " " ^ name) ^ ":"),
-    Pretty.fbrk, Proof.pretty_thm thm];
+    Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
 
-fun pretty_rule s thm =
+fun pretty_rule s ctxt thm =
   Pretty.block [Pretty.str (s ^ " to solve goal by exported rule:"),
-    Pretty.fbrk, Proof.pretty_thm thm];
+    Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
 
 in
 
-val print_result = Pretty.writeln o pretty_result;
+val print_result = Pretty.writeln oo pretty_result;
 
 fun cond_print_result_rule int =
-  if int then (print_result, priority o Pretty.string_of o pretty_rule "Attempt")
-  else (K (), K ());
+  if int then (print_result, priority oo (Pretty.string_of oo pretty_rule "Attempt"))
+  else (K (K ()), K (K ()));
 
 fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);
 
@@ -386,10 +386,11 @@
           (["Problem! Local statement will fail to solve any pending goal"] @
           (case exn of None => [] | Some e => [Toplevel.exn_message e]) @
           (case ! rule of None => [] | Some thm =>
-            [Pretty.string_of (pretty_rule "Failed attempt" thm)]))
+            [Pretty.string_of (pretty_rule "Failed attempt" (Proof.context_of state) thm)]))
           |> cat_lines |> warning;
         val check =
-          (fn () => Seq.pull (SkipProof.local_skip_proof (K (), fn thm => rule := Some thm) state))
+          (fn () => Seq.pull (SkipProof.local_skip_proof (K (K ()),
+            fn _ => fn thm => rule := Some thm) state))
           |> Library.setmp quick_and_dirty true
           |> Library.setmp proofs 0
           |> Library.transform_error;
@@ -507,7 +508,8 @@
     val (thy, res as {kind, name, thm}) = finish state;
   in
     if kind = "" orelse kind = Drule.internalK then ()
-    else (print_result res; Context.setmp (Some thy) (Present.result kind name) thm);
+    else (print_result (Proof.context_of state) res;
+      Context.setmp (Some thy) (Present.result kind name) thm);
     thy
   end);
 
@@ -535,8 +537,9 @@
 
 local
 
-fun cond_print_calc int thms =
-  if int then Pretty.writeln (Pretty.big_list "calculation:" (map Proof.pretty_thm thms))
+fun cond_print_calc int ctxt thms =
+  if int then
+    Pretty.writeln (Pretty.big_list "calculation:" (map (ProofContext.pretty_thm ctxt) thms))
   else ();
 
 fun proof''' f = Toplevel.proof' (f o cond_print_calc);

--- a/src/Pure/Isar/method.ML	Mon Nov 05 20:58:28 2001 +0100
+++ b/src/Pure/Isar/method.ML	Mon Nov 05 20:59:35 2001 +0100
@@ -16,7 +16,7 @@
 signature METHOD =
 sig
   include BASIC_METHOD
-  val trace: thm list -> unit
+  val trace: Proof.context -> thm list -> unit
   val print_global_rules: theory -> unit
   val print_local_rules: Proof.context -> unit
   val dest_global: theory attribute
@@ -99,17 +99,17 @@
   val refine_end: text -> Proof.state -> Proof.state Seq.seq
   val proof: text option -> Proof.state -> Proof.state Seq.seq
   val local_qed: bool -> text option
-    -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
-    -> Proof.state -> Proof.state Seq.seq
+    -> (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
+      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
   val local_terminal_proof: text * text option
-    -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
-    -> Proof.state -> Proof.state Seq.seq
-  val local_default_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
-    -> Proof.state -> Proof.state Seq.seq
-  val local_immediate_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
-    -> Proof.state -> Proof.state Seq.seq
-  val local_done_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
-    -> Proof.state -> Proof.state Seq.seq
+    -> (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
+      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
+  val local_default_proof: (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
+    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
+  val local_immediate_proof: (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
+    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
+  val local_done_proof: (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
+    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
   val global_qed: bool -> text option
     -> Proof.state -> theory * {kind: string, name: string, thm: thm}
   val global_terminal_proof: text * text option
@@ -132,9 +132,9 @@
 
 val trace_rules = ref false;
 
-fun trace rules =
+fun trace ctxt rules =
   if not (! trace_rules) orelse null rules then ()
-  else Pretty.writeln (Pretty.big_list "rules:" (map Display.pretty_thm rules));
+  else Pretty.writeln (Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules));
 
 
 
@@ -153,12 +153,11 @@
   | kind_name 3 = "elimination rules (elim)"
   | kind_name _ = "unknown";
 
-fun prt_rules sg (k, rs) =
-  Pretty.writeln (Pretty.big_list (kind_name k ^ ":")
-    (map (Display.pretty_thm_sg sg) (NetRules.rules rs)));
+fun prt_rules prt x (k, rs) =
+  Pretty.writeln (Pretty.big_list (kind_name k ^ ":") (map (prt x) (NetRules.rules rs)));
 
 in
-  fun print_rules sg rules = seq (prt_rules sg) (0 upto length rules - 1 ~~ rules);
+  fun print_rules prt x rules = seq (prt_rules prt x) (0 upto length rules - 1 ~~ rules);
 end;
 
 
@@ -173,7 +172,7 @@
   val copy = I;
   val prep_ext = I;
   fun merge x = map2 NetRules.merge x;
-  val print = print_rules;
+  val print = print_rules Display.pretty_thm_sg;
 end;
 
 structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
@@ -187,7 +186,7 @@
   val name = GlobalRulesArgs.name;
   type T = GlobalRulesArgs.T;
   val init = GlobalRules.get;
-  val print = print_rules o ProofContext.sign_of;
+  val print = print_rules ProofContext.pretty_thm;
 end;
 
 structure LocalRules = ProofDataFun(LocalRulesArgs);
@@ -352,7 +351,7 @@
       if not (null arg_rules) then arg_rules
       else find_erules facts (get elim_bangK) @ find_erules facts (get elimK) @
         find_rules goal (get intro_bangK) @ find_rules goal (get introK);
-  in trace rules; tac rules facts i end);
+  in trace ctxt rules; tac rules facts i end);
 
 fun meth tac x = METHOD (HEADGOAL o tac x);
 fun meth' tac x y = METHOD (HEADGOAL o tac x y);

--- a/src/Pure/Isar/obtain.ML	Mon Nov 05 20:58:28 2001 +0100
+++ b/src/Pure/Isar/obtain.ML	Mon Nov 05 20:59:35 2001 +0100
@@ -50,7 +50,7 @@
   in
     if not (null bads) then
       raise Proof.STATE ("Conclusion contains obtained parameters: " ^
-        space_implode " " (map (Sign.string_of_term sign) bads), state)
+        space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state)
     else if not (ObjectLogic.is_judgment sign (Logic.strip_assums_concl prop)) then
       raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
     else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule

--- a/src/Pure/Isar/proof.ML	Mon Nov 05 20:58:28 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Nov 05 20:59:35 2001 +0100
@@ -37,9 +37,6 @@
   val assert_backward: state -> state
   val assert_no_chain: state -> state
   val enter_forward: state -> state
-  val show_hyps: bool ref
-  val pretty_thm: thm -> Pretty.T
-  val pretty_thms: thm list -> Pretty.T
   val verbose: bool ref
   val print_state: int -> state -> unit
   val pretty_goals: bool -> state -> Pretty.T list
@@ -95,7 +92,8 @@
     -> term * (term list * term list) -> state -> state
   val at_bottom: state -> bool
   val local_qed: (state -> state Seq.seq)
-    -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) -> state -> state Seq.seq
+    -> (context -> {kind: string, name: string, thm: thm} -> unit) *
+      (context -> thm -> unit) -> state -> state Seq.seq
   val global_qed: (state -> state Seq.seq) -> state
     -> (theory * {kind: string, name: string, thm: thm}) Seq.seq
   val begin_block: state -> state
@@ -203,7 +201,6 @@
 val put_thms = map_context o ProofContext.put_thms;
 val put_thmss = map_context o ProofContext.put_thmss;
 val reset_thms = map_context o ProofContext.reset_thms;
-val assumptions = ProofContext.assumptions o context_of;
 val get_case = ProofContext.get_case o context_of;
 
 
@@ -308,18 +305,11 @@
 
 (** print_state **)
 
-val show_hyps = ProofContext.show_hyps;
-val pretty_thm = ProofContext.pretty_thm;
-
-fun pretty_thms [th] = pretty_thm th
-  | pretty_thms ths = Pretty.blk (0, Pretty.fbreaks (map pretty_thm ths));
-
-
 val verbose = ProofContext.verbose;
 
-fun pretty_facts _ None = []
-  | pretty_facts s (Some ths) =
-      [Pretty.big_list (s ^ "this:") (map pretty_thm ths), Pretty.str ""];
+fun pretty_facts _ _ None = []
+  | pretty_facts s ctxt (Some ths) =
+      [Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""];
 
 fun print_state nr (state as State (Node {context, facts, mode, goal = _}, nodes)) =
   let
@@ -334,7 +324,7 @@
       | subgoals n = ", " ^ string_of_int n ^ " subgoals";
       
     fun pretty_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) =
-      pretty_facts "using "
+      pretty_facts "using " context
         (if mode <> Backward orelse null goal_facts then None else Some goal_facts) @
       [Pretty.str ("goal (" ^ kind_name (sign_of state) kind ^
           (if name = "" then "" else " " ^ name) ^
@@ -343,7 +333,7 @@
 
     val ctxt_prts =
       if ! verbose orelse mode = Forward then ProofContext.pretty_context context
-      else if mode = Backward then ProofContext.pretty_prems context
+      else if mode = Backward then ProofContext.pretty_asms context
       else [];
 
     val prts =
@@ -352,8 +342,8 @@
         else "")), Pretty.str ""] @
      (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @
      (if ! verbose orelse mode = Forward then
-       (pretty_facts "" facts @ pretty_goal (find_goal state))
-      else if mode = ForwardChain then pretty_facts "picking " facts
+       (pretty_facts "" context facts @ pretty_goal (find_goal state))
+      else if mode = ForwardChain then pretty_facts "picking " context facts
       else pretty_goal (find_goal state))
   in Pretty.writeln (Pretty.chunks prts) end;
 
@@ -424,7 +414,7 @@
     val exp_tac = ProofContext.export true inner outer;
     fun exp_rule rule =
       let
-        val _ = print_rule rule;
+        val _ = print_rule outer rule;
         val thmq = FINDGOAL (refine_tac rule) thm;
       in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end;
   in raw_rule |> exp_tac |> (Seq.flat o Seq.map exp_rule) end;
@@ -455,13 +445,13 @@
     val {hyps, prop, sign, ...} = Thm.rep_thm thm;
     val tsig = Sign.tsig_of sign;
 
-    val casms = flat (map #1 (assumptions state));
+    val casms = flat (map #1 (ProofContext.assumptions_of (context_of state)));
     val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms);
   in
-    if not (null bad_hyps) then
-      err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
+    if not (null bad_hyps) then err ("Additional hypotheses:\n" ^
+        cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps))
     else if not (Pattern.matches (Sign.tsig_of (sign_of state)) (t, prop)) then
-      err ("Proved a different theorem: " ^ Sign.string_of_term sign prop)
+      err ("Proved a different theorem: " ^ ProofContext.string_of_term ctxt prop)
     else thm
   end;
 
@@ -608,7 +598,7 @@
       commas (map (Syntax.string_of_vname o #1) tvars), state);
     if null vars then ()
     else warning ("Goal statement contains unbound schematic variable(s): " ^
-      commas (map (Sign.string_of_term (sign_of state)) vars));
+      commas (map (ProofContext.string_of_term (context_of state')) vars));
     state'
     |> map_context (autofix prop)
     |> put_goal (Some (((kind, name, prop), ([], goal)), after_qed o map_context gen_binds))
@@ -700,7 +690,7 @@
       | Have atts => (atts, Seq.single)
       | _ => err_malformed "finish_local" state);
   in
-    print_result {kind = kind_name (sign_of state) kind, name = name, thm = result};
+    print_result goal_ctxt {kind = kind_name (sign_of state) kind, name = name, thm = result};
     outer_state
     |> auto_bind_facts name [ProofContext.generalize goal_ctxt outer_ctxt t]
     |> (fn st => Seq.map (fn res =>

--- a/src/Pure/Isar/skip_proof.ML	Mon Nov 05 20:58:28 2001 +0100
+++ b/src/Pure/Isar/skip_proof.ML	Mon Nov 05 20:59:35 2001 +0100
@@ -12,8 +12,8 @@
   val make_thm: theory -> term -> thm
   val cheat_tac: theory -> tactic
   val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
-  val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
-    -> Proof.state -> Proof.state Seq.seq
+  val local_skip_proof: (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
+    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
   val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
   val setup: (theory -> theory) list
 end;