# HG changeset patch
# User wenzelm
# Date 1140110758 -3600
# Node ID 77580f732e37730493af6b2e7523183d11aff5fa
# Parent  fce515f7759cdfaf8dea85d19d09d7821a0084e9
Proof.put_thms_internal;

diff -r fce515f7759c -r 77580f732e37 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Thu Feb 16 18:25:56 2006 +0100
+++ b/src/Pure/Isar/calculation.ML	Thu Feb 16 18:25:58 2006 +0100
@@ -62,7 +62,7 @@
 fun put_calculation calc =
   `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
      (CalculationData.map (apsnd (K (Option.map (rpair lev) calc))))))
-  #> Proof.put_thms (calculationN, calc);
+  #> Proof.put_thms_internal (calculationN, calc);