print calculation result in the context where the fact is actually defined -- proper externing;
misc tuning;

--- a/src/Pure/Isar/calculation.ML	Fri May 21 21:28:31 2010 +0200
+++ b/src/Pure/Isar/calculation.ML	Fri May 21 22:08:13 2010 +0200
@@ -14,7 +14,8 @@
   val sym_del: attribute
   val symmetric: attribute
   val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
-  val also_cmd: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
+  val also_cmd: (Facts.ref * Attrib.src list) list option ->
+    bool -> Proof.state -> Proof.state Seq.seq
   val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
   val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
     Proof.state -> Proof.state Seq.seq
@@ -27,7 +28,7 @@
 
 (** calculation data **)
 
-structure CalculationData = Generic_Data
+structure Data = Generic_Data
 (
   type T = (thm Item_Net.T * thm list) * (thm list * int) option;
   val empty = ((Thm.elim_rules, []), NONE);
@@ -37,7 +38,7 @@
 );
 
 fun print_rules ctxt =
-  let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
+  let val ((trans, sym), _) = Data.get (Context.Proof ctxt) in
     [Pretty.big_list "transitivity rules:"
         (map (Display.pretty_thm ctxt) (Item_Net.content trans)),
       Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
@@ -48,7 +49,7 @@
 (* access calculation *)
 
 fun get_calculation state =
-  (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of
+  (case #2 (Data.get (Context.Proof (Proof.context_of state))) of
     NONE => NONE
   | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
 
@@ -56,7 +57,7 @@
 
 fun put_calculation calc =
   `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
-     (CalculationData.map (apsnd (K (Option.map (rpair lev) calc))))))
+     (Data.map (apsnd (K (Option.map (rpair lev) calc))))))
   #> Proof.put_thms false (calculationN, calc);
 
 
@@ -65,22 +66,22 @@
 
 (* add/del rules *)
 
-val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.update);
-val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.remove);
+val trans_add = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update);
+val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);
 
 val sym_add =
-  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
+  Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.add_thm)
   #> Context_Rules.elim_query NONE;
 
 val sym_del =
-  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm)
+  Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.del_thm)
   #> Context_Rules.rule_del;
 
 
 (* symmetric *)
 
 val symmetric = Thm.rule_attribute (fn x => fn th =>
-  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
+  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (Data.get x)))) of
     ([th'], _) => Drule.zero_var_indexes th'
   | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
@@ -103,28 +104,31 @@
 
 (** proof commands **)
 
-fun err_if b msg = if b then error msg else ();
-
 fun assert_sane final =
   if final then Proof.assert_forward else Proof.assert_forward_or_chain;
 
-fun maintain_calculation false calc = put_calculation (SOME calc)
-  | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
-
-fun print_calculation false _ _ = ()
-  | print_calculation true ctxt calc = Pretty.writeln
-      (ProofContext.pretty_fact ctxt (ProofContext.full_name ctxt (Binding.name calculationN), calc));
+fun maintain_calculation int final calc state =
+  let
+    val state' = put_calculation (SOME calc) state;
+    val ctxt' = Proof.context_of state';
+    val _ =
+      if int then
+        Pretty.writeln
+          (ProofContext.pretty_fact ctxt'
+            (ProofContext.full_name ctxt' (Binding.name calculationN), calc))
+      else ();
+  in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
 
 
 (* also and finally *)
 
-val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of;
+val get_rules = #1 o Data.get o Context.Proof o Proof.context_of;
 
 fun calculate prep_rules final raw_rules int state =
   let
     val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
     val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
-    fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
+    fun projection ths th = exists (curry eq_prop th) ths;
 
     val opt_rules = Option.map (prep_rules state) raw_rules;
     fun combine ths =
@@ -141,11 +145,12 @@
       (case get_calculation state of
         NONE => (true, Seq.single facts)
       | SOME calc => (false, Seq.map single (combine (calc @ facts))));
+
+    val _ = initial andalso final andalso error "No calculation yet";
+    val _ = initial andalso is_some opt_rules andalso
+      error "Initial calculation -- no rules to be given";
   in
-    err_if (initial andalso final) "No calculation yet";
-    err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
-    calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
-        state |> maintain_calculation final calc))
+    calculations |> Seq.map (fn calc => maintain_calculation int final calc state)
   end;
 
 val also = calculate (K I) false;
@@ -164,11 +169,8 @@
         NONE => (true, [])
       | SOME thms => (false, thms));
     val calc = thms @ facts;
-  in
-    err_if (initial andalso final) "No calculation yet";
-    print_calculation int (Proof.context_of state) calc;
-    state |> maintain_calculation final calc
-  end;
+    val _ = initial andalso final andalso error "No calculation yet";
+  in maintain_calculation int final calc state end;
 
 val moreover = collect false;
 val ultimately = collect true;