# HG changeset patch
# User wenzelm
# Date 1164128864 -3600
# Node ID 0d562bf8ac3e72fe846d7656ac663863e1749be1
# Parent  8f71e2b3fd92b531f88ab8212c31d752ed12c813
renamed Proof.put_thms_internal to Proof.put_thms;

diff -r 8f71e2b3fd92 -r 0d562bf8ac3e src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Nov 21 18:07:43 2006 +0100
+++ b/src/Pure/Isar/calculation.ML	Tue Nov 21 18:07:44 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_internal (calculationN, calc);
+  #> Proof.put_thms (calculationN, calc);